eRk_le_encard

Mathlib.Combinatorics.Matroid.Rank.ENat

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

← MathLib Explorer

English

For any X, eRk(X) ≤ encard(X).

Русский

Для любого X выполняется eRk(X) ≤ encard(X).

LaTeX

$$$ M.eRk(X) \\le X.encard $$$

Lean4

theorem eRk_le_encard (M : Matroid α) (X : Set α) : M.eRk X ≤ X.encard :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [hI.eRk_eq_encard]
  exact encard_mono hI.subset

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

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

Разделы

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

Аффилиация

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