English
If M has finite rank, then M is finitary (every independent set has a finite base augmentations).
Русский
Если ранг матроида конечен, то он конечносодержательный: каждый независимый набор имеет конечную аугментацию в базу.
LaTeX
$$M.RankFinite ⇒ M.Finitary$$
Lean4
instance finitary_of_rankFinite {M : Matroid α} [RankFinite M] : Finitary M where
indep_of_forall_finite I
hI := by
refine I.finite_or_infinite.elim (hI _ Subset.rfl) (fun h ↦ False.elim ?_)
obtain ⟨B, hB⟩ := M.exists_isBase
obtain ⟨I₀, hI₀I, hI₀fin, hI₀card⟩ := h.exists_subset_ncard_eq (B.ncard + 1)
obtain ⟨B', hB', hI₀B'⟩ := (hI _ hI₀I hI₀fin).exists_isBase_superset
have hle := ncard_le_ncard hI₀B' hB'.finite
rw [hI₀card, hB'.ncard_eq_ncard_of_isBase hB, Nat.add_one_le_iff] at hle
exact hle.ne rfl
