encard_eq_encard

Mathlib.Combinatorics.Matroid.Minor.Restrict

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

← MathLib Explorer

English

If I and J are bases of M on X in the IsBasis' sense, their encard are equal: I.encard = J.encard.

Русский

Если I и J — базы M на X в смысле IsBasis', то I.encard = J.encard.

LaTeX

$$I.encard = J.encard$$

Lean4

theorem encard_eq_encard (hI : M.IsBasis' I X) (hJ : M.IsBasis' J X) : I.encard = J.encard := by
  rw [← isBase_restrict_iff'] at hI hJ; exact hI.encard_eq_encard_of_isBase hJ

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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