uniqueBaseOn_rankFinite — Mathlib

English

If I is finite, then the matroid uniqueBaseOn I E has finite rank.

Русский

Если I конечно, то матроид uniqueBaseOn I E имеет конечный ранг.

LaTeX

$$$I \text{ finite } \Rightarrow \mathrm{RankFinite}(\mathrm{uniqueBaseOn}(I,E))$$$

Lean4

theorem uniqueBaseOn_rankFinite (hI : I.Finite) : RankFinite (uniqueBaseOn I E) :=
  by
  rw [← uniqueBaseOn_inter_ground_eq]
  refine ⟨I ∩ E, ?_⟩
  rw [uniqueBaseOn_isBase_iff inter_subset_right, and_iff_right rfl]
  exact hI.subset inter_subset_left

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