upperClosure

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#UpperSet.upperClosure

English

For an upper set s, the closure map preserves the element, i.e., upperClosure (s) = s.

Русский

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

LaTeX

$$UpperSet[s] → upperClosure (s) = s$$

Lean4

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

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

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

Разделы

Аффилиация

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