indep_iff_eRk_eq_encard_of_finite

English

For a finite set I, independence is equivalent to the equality eRk I = I.encard: M.Indep I iff M.eRk I = I.encard.

Русский

Для конечного множества I независимость эквивалентна равенству eRk I и encard I: M.Indep I ⇔ M.eRk I = I.encard.

LaTeX

$$$I \\text{ finite} \\;\\Rightarrow\\; M.Indep I \\;\\Leftrightarrow\\; M.eRk I = I.encard$$$

Lean4

theorem indep_iff_eRk_eq_encard_of_finite (hI : I.Finite) : M.Indep I ↔ M.eRk I = I.encard :=
  by
  refine ⟨fun h ↦ by rw [h.eRk_eq_encard], fun h ↦ ?_⟩
  obtain ⟨J, hJ⟩ := M.exists_isBasis' I
  rw [← hI.eq_of_subset_of_encard_le' hJ.subset]
  · exact hJ.indep
  rw [← h, ← hJ.eRk_eq_encard]

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