restrict_eRk_eq' — Mathlib

English

If I is a basis for X, then for every Y, eRk(I ∪ Y) = eRk(X ∪ Y).

Русский

Если I является базисом множества X, тогда для любого Y выполняется eRk(I ∪ Y) = eRk(X ∪ Y).

LaTeX

$$$ M.IsBasis' I X \\Rightarrow \\forall Y, M.eRk(I \\cup Y) = M.eRk(X \\cup Y) $$$

Lean4

/-- A version of `Matroid.restrict_eRk_eq` with no `X ⊆ R` hypothesis and thus a less simple RHS. -/
@[simp]
theorem restrict_eRk_eq' (M : Matroid α) (R X : Set α) : (M ↾ R).eRk X = M.eRk (X ∩ R) :=
  by
  obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X
  rw [hI.eRk_eq_encard]
  rw [isBasis'_iff_isBasis_inter_ground, isBasis_restrict_iff', restrict_ground_eq] at hI
  rw [← eRk_inter_ground, ← hI.1.eRk_eq_encard]

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