En ℝ, x² = y² → x = y ∨ x = -y
Demostrar con Lean4 que en \(ℝ\),
\[x² = y² → x = y ∨ x = -y\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example (h : x^2 = y^2) : x = y ∨ x = -y := by sorry |