encard_eq_encard_of_isBase

Mathlib.Combinatorics.Matroid.Basic

URI: https://scilib.ai/kg/mathlib#Matroid.IsBase.encard_eq_encard_of_isBase

← MathLib Explorer

English

If B1 and B2 are bases of M, then their encard are equal: encard(B1) = encard(B2).

Русский

Если B1 и B2 — базы M, то их encard равны: encard(B1) = encard(B2).

LaTeX

$$$(hB_1 : M.IsBase B_1) \to (hB_2 : M.IsBase B_2) : B_1.encard = B_2.encard$$$

Lean4

theorem encard_eq_encard_of_isBase (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) : B₁.encard = B₂.encard := by
  rw [M.isBase_exchange.encard_isBase_eq hB₁ hB₂]

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

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

Разделы

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

Аффилиация

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