eq_of_subset_isBase

Mathlib.Combinatorics.Matroid.Basic

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

English

If B1 and B2 are bases and B1 ⊆ B2, then B1 = B2.

Русский

Если B1 и B2 — базы и B1 ⊆ B2, то B1 = B2.

LaTeX

$$$$ hB_1 : M.IsBase B_1 \to hB_2 : M.IsBase B_2 \to B_1 \subseteq B_2 \Rightarrow B_1 = B_2 $$$$

Lean4

theorem eq_of_subset_isBase (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (hB₁B₂ : B₁ ⊆ B₂) : B₁ = B₂ :=
  M.isBase_exchange.antichain hB₁ hB₂ hB₁B₂

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

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

Разделы

Аффилиация

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