cardinalMk_le_isBasis

Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

English

If I is independent, J is a base of X, and I ⊆ X, then |I| ≤ |J|.

Русский

Если I — независимый, 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 :=
  hI.cardinalMk_le_isBasis' hJ.isBasis' hIX

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

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

Разделы

Аффилиация

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