closure

Mathlib.Combinatorics.Matroid.Loop

URI: https://scilib.ai/kg/mathlib#Matroid.IsLoop.closure

English

The isLoop.closure lemma: closure of {e} equals closure of e’s loop source; equivalently, closure of {e} equals closure of {e}.

Русский

Лемма isLoop.closure: замыкание множества {e} равно замыканию петли e.

LaTeX

$$$ M.IsLoop e \Rightarrow M.closure\{e\} = M.loops $$$

Lean4

theorem closure (he : M.IsLoop e) : M.closure { e } = M.loops :=
  closure_eq_loops_of_subset (singleton_subset_iff.mpr he)

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

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

Разделы

Аффилиация

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