cRk_mono — Mathlib

English

The restricted rank equals the cRk of X: (M|X).cRank = M.cRk X.

Русский

Ограниченный ранг равен cRk X: (M|X).cRank = M.cRk X.

LaTeX

$$$(M \\restriction X).\\mathrm{cRank} = M.\\mathrm{cRk} X$$$

Lean4

theorem cRk_mono (M : Matroid α) : Monotone M.cRk :=
  by
  simp only [Monotone, le_eq_subset, cRk_le_iff]
  intro X Y hXY I hIX
  obtain ⟨J, hJ, hIJ⟩ := hIX.indep.subset_isBasis'_of_subset (hIX.subset.trans hXY)
  exact (mk_le_mk_of_subset hIJ).trans hJ.cardinalMk_le_cRk

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