eRk_lt_encard_of_dep_of_finite

Mathlib.Combinatorics.Matroid.Rank.ENat

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

← MathLib Explorer

English

If X is finite and M.Dep X, then M.eRk X < X.encard.

Русский

Если X конечно и X зависимо, то eRk X меньше encard X.

LaTeX

$$If $X$ is finite and $M.Dep X$, then $M.eRk X < X.encard$.$$

Lean4

theorem eRk_lt_encard_of_dep_of_finite (h : X.Finite) (hX : M.Dep X) : M.eRk X < X.encard :=
  lt_of_le_of_ne (M.eRk_le_encard X) fun h' ↦ ((indep_iff_eRk_eq_encard_of_finite h).mpr h').not_dep hX

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

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

Разделы

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

Аффилиация

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