spanning_iff_eRk_le' — Mathlib

English

For RankFinite M, spanning X is equivalent to eRank dominance and ground inclusion: M.Spanning X ↔ eRank ≤ eRk X and X ⊆ E.

Русский

Для RankFinite матроида M: M.Spanning X эквивалентно тому, что eRank доминирует над eRk X и X ⊆ E.

LaTeX

$$For RankFinite $M$, $M.Spanning X \\iff (M.eRank \\le M.eRk X) \\wedge X \\subseteq M.E$.$$

Lean4

theorem spanning_iff_eRk_le' [RankFinite M] : M.Spanning X ↔ M.eRank ≤ M.eRk X ∧ X ⊆ M.E :=
  by
  refine ⟨fun h ↦ ⟨h.eRk_eq.symm.le, h.subset_ground⟩, fun ⟨h, hX⟩ ↦ ?_⟩
  obtain ⟨I, hI⟩ := M.exists_isBasis X
  exact (hI.indep.isBase_of_eRk_ge hI.indep.finite (h.trans hI.eRk_eq_eRk.symm.le)).spanning_of_superset hI.subset

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