cRk_restrict_subset — Mathlib

English

For any M and X,Y, the restricted rank equals the rank of the intersection: (M|X).cRk Y = M.cRk (X ∩ Y).

Русский

Для любого M и X,Y: (M|X).cRk Y = M.cRk(X ∩ Y).

LaTeX

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

Lean4

theorem cRk_restrict_subset (M : Matroid α) (hYX : Y ⊆ X) : (M ↾ X).cRk Y = M.cRk Y :=
  by
  have aux : ∀ ⦃I⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y :=
    by
    simp_rw [isBasis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
    exact fun I h ↦ h.subset.trans hYX
  simp_rw [le_antisymm_iff, cRk_le_iff]
  exact ⟨fun I hI ↦ (aux.2 hI).cardinalMk_le_cRk, fun I hI ↦ (aux.1 hI).cardinalMk_le_cRk⟩

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