encard_le_eRk_of_subset

Mathlib.Combinatorics.Matroid.Rank.ENat

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

English

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

Русский

Если I X является базисом 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_eRk_of_subset (hI : M.Indep I) (hIX : I ⊆ X) : I.encard ≤ M.eRk X :=
  hI.eRk_eq_encard ▸ M.eRk_mono hIX

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

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

Разделы

Аффилиация

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