closure

Mathlib.Combinatorics.Matroid.Closure

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

English

A set F is flat iff its closure equals itself.

Русский

Множество F плоско тогда и только тогда, когда его замыкание равно самому F.

LaTeX

$$$M.IsFlat F \iff M.closure F = F$$$

Lean4

theorem closure (hF : M.IsFlat F) : M.closure F = F :=
  (sInter_subset_of_mem (by simpa)).antisymm (M.subset_closure F)

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

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

Разделы

Аффилиация

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