eRank_def

Mathlib.Combinatorics.Matroid.Rank.ENat

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

English

The eRank of M equals the eRk of the ground set M.E.

Русский

Ранк eRank матроидa равен eRk по множеству оснований M.E.

LaTeX

$$$ M.eRank = M.eRk(M.E) $$$

Lean4

theorem eRank_def (M : Matroid α) : M.eRank = M.eRk M.E := by rw [eRk, restrict_ground_eq_self]

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

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

Разделы

Аффилиация

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