cRk_inter_ground — Mathlib · SciLib

English

Intersecting with the ground does not change cRk: cRk(X ∩ E) = cRk(X).

Русский

Пересечение с опорной множестом не изменяет cRk: cRk(X ∩ E) = cRk(X).

LaTeX

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

Lean4

@[simp]
theorem cRk_inter_ground (M : Matroid α) (X : Set α) : M.cRk (X ∩ M.E) = M.cRk X :=
  (M.cRk_le_of_subset inter_subset_left).antisymm <| cRk_le_iff.2 fun _ h ↦ h.isBasis_inter_ground.cardinalMk_le_cRk

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