ofIsBaseOfFinite_E

Mathlib.Combinatorics.Matroid.IndepAxioms

URI: https://scilib.ai/kg/mathlib#Matroid.ofIsBaseOfFinite_E

← MathLib Explorer

English

The E-field of Matroid.ofIsBaseOfFinite equals E.

Русский

Поле E у Matroid.ofIsBaseOfFinite равно E.

LaTeX

$$$(Matroid.ofIsBaseOfFinite\\ hE\\ IsBase\\ exists_isBase\\ subset_ground).E = E$$$

Lean4

@[simp]
theorem ofIsBaseOfFinite_E {E : Set α} (hE : E.Finite) IsBase exists_isBase isBase_exchange subset_ground :
    (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).E = E :=
  rfl

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

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

Разделы

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

Аффилиация

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