eRk_freeOn — Mathlib

English

If X ⊆ Y, then the eRk of X in the free matroid on Y equals the cardinality of X: (freeOn Y).eRk X = X.encard.

Русский

Если X ⊆ Y, то eRk(X) в свободном матроиде над Y равен кардинальности X: (freeOn Y).eRk X = X.encard.

LaTeX

$$$ X \\subseteq Y \\implies (\\mathrm{freeOn}~Y).\\mathrm{eRk}~X = X.encard $$$

Lean4

theorem eRk_freeOn (hXY : X ⊆ Y) : (freeOn Y).eRk X = X.encard :=
  by
  obtain ⟨I, hI⟩ := (freeOn Y).exists_isBasis X
  rw [hI.eRk_eq_encard, (freeOn_indep hXY).eq_of_isBasis hI]

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