encard_eq_eRank

Mathlib.Combinatorics.Matroid.Rank.ENat

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

← MathLib Explorer

English

If B is a base of M, then B.encard = M.eRank.

Русский

Если B — база M, то B.encard равно eRank(M).

LaTeX

$$$ B.encard = M.eRank $$$

Lean4

theorem encard_eq_eRank (hB : M.IsBase B) : B.encard = M.eRank := by
  simp [eRank, show ∀ B' : { B // M.IsBase B }, B'.1.encard = B.encard from fun B' ↦ B'.2.encard_eq_encard_of_isBase hB]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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