cardinalMk_eq_cRk

Mathlib.Combinatorics.Matroid.Rank.Cardinal

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis'.cardinalMk_eq_cRk

English

If I is a Basis' I X, then |I| = cRk(X).

Русский

Если I — Basis' I X, то |I| = cRk(X).

LaTeX

$$$|I| = cRk(X)$$$

Lean4

theorem cardinalMk_eq_cRk (hIX : M.IsBasis' I X) : #I = M.cRk X := by
  rw [cRk, (isBase_restrict_iff'.2 hIX).cardinalMk_eq_cRank]

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

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

Разделы

Аффилиация

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