English
For left inner product, zero on x implies x = 0; and conversely.
Русский
Если ⟪x,·⟫ равен нулю на x, то x = 0; и наоборот.
LaTeX
$$$\langle x, x\rangle = 0 \iff x = 0$$$
Lean4
/-- Normed group structure constructed from an `InnerProductSpace.Core` structure -/
def toNormedAddCommGroup : NormedAddCommGroup F :=
AddGroupNorm.toNormedAddCommGroup
{ toFun := fun x => √(re ⟪x, x⟫)
map_zero' := by simp only [sqrt_zero, inner_zero_right, map_zero]
neg' := fun x => by simp only [inner_neg_left, neg_neg, inner_neg_right]
add_le' := fun x y => by
have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_norm _ _
have h₂ : re ⟪x, y⟫ ≤ ‖⟪x, y⟫‖ := re_le_norm _
have h₃ : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ := h₂.trans h₁
have h₄ : re ⟪y, x⟫ ≤ ‖x‖ * ‖y‖ := by rwa [← inner_conj_symm, conj_re]
have : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖) :=
by
simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]
linarith
exact nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this
eq_zero_of_map_eq_zero' := fun _ hx => normSq_eq_zero.1 <| (sqrt_eq_zero inner_self_nonneg).1 hx }
