independent_iff — Mathlib

English

Independent f is equivalent to iSupIndep of the submodules (f i).submodule.

Русский

Независимость f эквивалентна iSupIndep подмодулей (f i).submodule.

LaTeX

$$$Independent(f) \\iff iSupIndep (fun i => (f(i)).submodule)$$$

Lean4

/-- A family of points in a projective space is independent if and only if the representative
vectors determined by the family are linearly independent. -/
theorem independent_iff : Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f) :=
  by
  refine ⟨?_, fun h => ?_⟩
  · rintro ⟨ff, hff, hh⟩
    choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
    convert hh.units_smul a
    ext i
    exact (ha i).symm
  · convert Independent.mk _ _ h
    · simp only [mk_rep, Function.comp_apply]
    · intro i
      apply rep_nonzero

Похожие утверждения