closure_eq_loops_of_subset

Mathlib.Combinatorics.Matroid.Loop

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

← MathLib Explorer

English

The closure of the set of loops equals the set of loops: closure(M.loops) = M.loops.

Русский

Замыкание множества петель равно самому множеству петель.

LaTeX

$$$ M.closure M.loops = M.loops $$$

Lean4

theorem closure_eq_loops_of_subset (h : X ⊆ M.loops) : M.closure X = M.loops :=
  (closure_subset_closure_of_subset_closure h).antisymm (M.closure_mono (empty_subset _))

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

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

Разделы

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

Аффилиация

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