encard_le_eRank

Mathlib.Combinatorics.Matroid.Rank.ENat

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.encard_le_eRank

English

If I is a basis for X, then for all Y, eRk(I ∪ Y) = eRk(X ∪ Y).

Русский

Если I является базисом X, то для любого Y выполнится eRk(I ∪ Y) = eRk(X ∪ Y).

LaTeX

$$$ (hIX : M.IsBasis I X) (Y) : M.eRk(I \\cup Y) = M.eRk(X \\cup Y) $$$

Lean4

theorem encard_le_eRank (hI : M.Indep I) : I.encard ≤ M.eRank :=
  by
  rw [← hI.eRk_eq_encard, eRank_def]
  exact M.eRk_mono hI.subset_ground

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

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

Разделы

Аффилиация

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