eRk_mono — Mathlib

English

The rank map eRk is monotone: if X ⊆ Y then eRk(X) ≤ eRk(Y).

Русский

РангeRk монотонен: если X ⊆ Y, то eRk(X) ≤ eRk(Y).

LaTeX

$$$ X \\subseteq Y \\Rightarrow M.eRk(X) \\le M.eRk(Y) $$$

Lean4

theorem eRk_mono (M : Matroid α) : Monotone M.eRk :=
  by
  rintro X Y (hXY : X ⊆ Y)
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)
  rw [hI.eRk_eq_encard, hJ.eRk_eq_encard]
  exact encard_mono hIJ

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