theorem
proved
tactic proof
spatialNormSq_eq_zero_iff
show as:
view Lean formalization →
formal statement (Lean)
135theorem spatialNormSq_eq_zero_iff (x : Fin 4 → ℝ) : spatialNormSq x = 0 ↔ x 1 = 0 ∧ x 2 = 0 ∧ x 3 = 0 := by
proof body
Tactic-mode proof.
136 unfold spatialNormSq
137 constructor
138 · intro h
139 have h1 := sq_nonneg (x 1)
140 have h2 := sq_nonneg (x 2)
141 have h3 := sq_nonneg (x 3)
142 have h1_zero : x 1 ^ 2 = 0 := by linarith
143 have h2_zero : x 2 ^ 2 = 0 := by linarith
144 have h3_zero : x 3 ^ 2 = 0 := by linarith
145 simp only [sq_eq_zero_iff] at h1_zero h2_zero h3_zero
146 exact ⟨h1_zero, h2_zero, h3_zero⟩
147 · intro h
148 simp [h]
149
150/-- Spatial radius `r = √(x₁² + x₂² + x₃²)`. -/