English
For any I with RankFinite (Rk finite), independence is equivalent to eRk I = I.encard: M.Indep I ↔ M.eRk I = I.encard.
Русский
Для произвольного I с конечной ранговостью независимость эквивалентна eRk I = I.encard: M.Indep I ⇔ M.eRk I = I.encard.
LaTeX
$$$\\text{RankFinite} \\ M \\ I \\Rightarrow M.Indep I \\Leftrightarrow M.eRk I = I.encard$$$
Lean4
/-- In a matroid known to have finite rank, `Matroid.indep_iff_eRk_eq_encard_of_finite`
is true without the finiteness assumption. -/
theorem indep_iff_eRk_eq_encard [M.RankFinite] : M.Indep I ↔ M.eRk I = I.encard :=
by
refine ⟨Indep.eRk_eq_encard, fun h ↦ ?_⟩
obtain hfin | hinf := I.finite_or_infinite
· rwa [indep_iff_eRk_eq_encard_of_finite hfin]
rw [hinf.encard_eq] at h
exact False.elim <| (M.isRkFinite_set I).eRk_lt_top.ne h
