encard_compl_eq

Mathlib.Combinatorics.Matroid.Rank.ENat

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

English

For a base B, the encard of the ground complement M.E \\ B equals the dual eRank: (M.E \\ B).encard = M✶.eRank.

Русский

Для базы B величина encard множества E \ B равна eRank двойственного: (M.E \\ B).encard = M✶.eRank.

LaTeX

$$$ (M.E \\ B).encard = M^{\\ast}.eRank $$$

Lean4

theorem encard_compl_eq (hB : M.IsBase B) : (M.E \ B).encard = M✶.eRank :=
  (hB.compl_isBase_dual).encard_eq_eRank

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

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

Разделы

Аффилиация

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