eRk_eq_eRank — Mathlib · SciLib

English

Let M be a matroid on α with ground set E. If X is a subset of α that contains the ground E (i.e., E ⊆ X), then the extended rank eRk of X equals the rank eRank of M.

Русский

Пусть M — матроид на множество α, опорное множество E. Пусть X ⊆ α удовлетворяет E ⊆ X. Тогда расширенный ранг eRk множества X равен рангу eRank матоида M.

LaTeX

$$$ M.E \\subseteq X \\Rightarrow M.eRk(X) = M.eRank $$$

Lean4

theorem eRk_eq_eRank (hX : M.E ⊆ X) : M.eRk X = M.eRank := by
  rw [← eRk_inter_ground, inter_eq_self_of_subset_right hX, eRank_def]

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