indep_of_encard_le_eRk — Mathlib

English

If I is IsRkFinite and encard I ≤ eRk I, then I is independent: M.IsRkFinite I → encard I ≤ eRk I → M.Indep I.

Русский

Если I конечна по рангу и encard I ≤ eRk I, то I независима: M.IsRkFinite I → encard I ≤ eRk I → M.Indep I.

LaTeX

$$$M.IsRkFinite I \\rightarrow encard I \\le M.eRk I \\rightarrow M.Indep I$$$

Lean4

theorem indep_of_encard_le_eRk (hX : M.IsRkFinite I) (h : encard I ≤ M.eRk I) : M.Indep I :=
  by
  rw [indep_iff_eRk_eq_encard_of_finite _]
  · exact (M.eRk_le_encard I).antisymm h
  simpa using h.trans_lt hX.eRk_lt_top

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