cardinalMk_le_isBasis'

Mathlib.Combinatorics.Matroid.Rank.Cardinal

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.cardinalMk_le_isBasis'

← MathLib Explorer

English

If I is independent, J is Basis' J X, and I ⊆ X, then |I| ≤ |J|.

Русский

Если I — независимый, J — Basis' J X и I ⊆ X, тогда |I| ≤ |J|.

LaTeX

$$$|I| \le |J|$$$

Lean4

theorem cardinalMk_le_isBasis' (hI : M.Indep I) (hJ : M.IsBasis' J X) (hIX : I ⊆ X) : #I ≤ #J :=
  have ⟨_J', hJ', hIJ'⟩ := hI.subset_isBasis'_of_subset hIX
  hJ'.cardinalMk_eq hJ ▸ mk_le_mk_of_subset hIJ'

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

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

Разделы

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

Аффилиация

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