eRk_eq_eRank

Mathlib.Combinatorics.Matroid.Rank.ENat

URI: https://scilib.ai/kg/mathlib#Matroid.IsBase.eRk_eq_eRank

English

If B is a base, then M.eRk B = M.eRank.

Русский

Если B — база, то eRk(B) = eRank(M).

LaTeX

$$$ M.IsBase(B) \\Rightarrow M.eRk B = M.eRank $$$

Lean4

theorem eRk_eq_eRank (hB : M.IsBase B) : M.eRk B = M.eRank := by
  rw [hB.indep.eRk_eq_encard, eRank_def, hB.isBasis_ground.encard_eq_eRk]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru