closure_def

Mathlib.Combinatorics.Matroid.Closure

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

English

The closure of X is the intersection of all flats containing X ∩ M.E.

Русский

Замыкание X есть пересечение всех плоскостей, содержащих X ∩ M.E.

LaTeX

$$$M.closure X = \bigcap\{ F \mid M.IsFlat F ∧ X \cap M.E ⊆ F \}$$$

Lean4

theorem closure_def (M : Matroid α) (X : Set α) : M.closure X = ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F} :=
  rfl

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

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

Разделы

Аффилиация

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