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 |
Demostración en lenguaje natural
Al ser \(f\) suprayectiva, existe un \(y\) tal que \(f(y) = 3\). Por tanto, \(f(y)² = 9\).
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
import Mathlib.Data.Real.Basic open Function example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, (f x)^2 = 9 := by cases' h 3 with y hy -- y : ℝ -- hy : f y = 3 use y -- ⊢ f y ^ 2 = 9 rw [hy] -- ⊢ 3 ^ 2 = 9 norm_num |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 31.
