eRk_lt_encard

Mathlib.Combinatorics.Matroid.Rank.ENat

URI: https://scilib.ai/kg/mathlib#Matroid.Dep.eRk_lt_encard

← MathLib Explorer

English

Under RankFinite, if M.Dep X then M.eRk X < X.encard.

Русский

При RankFinite, если M.Dep X, то eRk X < encard X.

LaTeX

$$[M.RankFinite] (M.Dep X) → M.eRk X < X.encard$$

Lean4

theorem eRk_lt_encard [M.RankFinite] (hX : M.Dep X) : M.eRk X < X.encard :=
  by
  refine (M.eRk_le_encard X).lt_of_ne ?_
  rw [ne_eq, ← indep_iff_eRk_eq_encard]
  exact hX.not_indep

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

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

Разделы

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

Аффилиация

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