En ℝ, x² + y² = 0 ↔ x = 0 ∧ y = 0
Demostrar con Lean4 que si \(x, y ∈ ℝ\), entonces
\[ x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example : x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 := by sorry |