English
Under orthogonality, the invariants imply independence: for any x, ⟪x_i, x_i⟫ = 0 implies x_i = 0.
Русский
При ортогональности независимость следует из нулевых попарных скалярных произведений: если для каждого i ⟪x_i, x_i⟫ = 0, то x_i = 0.
LaTeX
$$iSupIndep V$$
Lean4
/-- An orthogonal family forms an independent family of subspaces; that is, any collection of
elements each from a different subspace in the family is linearly independent. In particular, the
pairwise intersections of elements of the family are 0. -/
theorem independent {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) :
iSupIndep V := by
classical
apply iSupIndep_of_dfinsupp_lsum_injective
refine LinearMap.ker_eq_bot.mp ?_
rw [Submodule.eq_bot_iff]
intro v hv
rw [LinearMap.mem_ker] at hv
ext i
suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using this
calc
⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using (hV.inner_right_dfinsupp v i (v i)).symm
_ = 0 := by simp only [hv, inner_zero_right]
