lowerClosure

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#LowerSet.lowerClosure

English

For a lower set s, the closure map preserves the element, i.e., lowerClosure (s) = s.

Русский

Для нижнего множества s отображение нижнего замыкания сохраняет элемент, то есть lowerClosure s = s.

LaTeX

$$LowerSet[s] → lowerClosure (s) = s$$

Lean4

@[simp]
protected theorem lowerClosure (s : LowerSet α) : lowerClosure (s : Set α) = s :=
  SetLike.coe_injective s.2.lowerClosure

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

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

Разделы

Аффилиация

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