toENat_cRk_eq

Mathlib.Combinatorics.Matroid.Rank.Cardinal

URI: https://scilib.ai/kg/mathlib#Matroid.toENat_cRk_eq

English

For any X, (M.cRk X).toENat = M.eRk X.

Русский

Для любого X выполняется: (cRk(X)).toENat = eRk(X).

LaTeX

$$$ (M.cRk X).toENat = M.eRk X $$$

Lean4

@[simp]
theorem toENat_cRk_eq (M : Matroid α) (X : Set α) : (M.cRk X).toENat = M.eRk X := by rw [cRk, toENat_cRank_eq, eRk]

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

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

Разделы

Аффилиация

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