Si f: ℝ → ℝ es suprayectiva, entonces ∃x ∈ ℝ tal que f(x)² = 9
Demostrar con Lean4 que si \(f: ℝ → ℝ\) es suprayectiva, entonces \(∃x ∈ ℝ\) tal que \(f(x)² = 9\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic open Function example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, (f x)^2 = 9 := by sorry |
Read More «Si f: ℝ → ℝ es suprayectiva, entonces ∃x ∈ ℝ tal que f(x)² = 9»