eRk_eq_encard

Mathlib.Combinatorics.Matroid.Rank.ENat

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis.eRk_eq_encard

English

If I is a basis' for X, then M.eRk X = I.encard.

Русский

Если I является базой' для X, то eRk(X) = I.encard.

LaTeX

$$$ (hIX) \\Rightarrow M.eRk X = I.encard $$$

Lean4

theorem eRk_eq_encard (hIX : M.IsBasis I X) : M.eRk X = I.encard := by rw [← hIX.eRk_eq_eRk, hIX.indep.eRk_eq_encard]

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

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

Разделы

Аффилиация

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