eRk_eq_eRk

Mathlib.Combinatorics.Matroid.Rank.ENat

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

English

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

Русский

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

LaTeX

$$$ M.IsBasis' I X \\Rightarrow M.eRk I = M.eRk X $$$

Lean4

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

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

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

Разделы

Аффилиация

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