upperClosure

Mathlib.Order.UpperLower.Closure

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

English

If s is an upper set, then the upper closure of s equals s.

Русский

Если s — верхнее множество, то верхнее замыкание s равно самому s.

LaTeX

$$IsUpperSet(s) ⇒ upperClosure(s) = s$$

Lean4

protected theorem upperClosure (hs : IsUpperSet s) : ↑(upperClosure s) = s :=
  (upperClosure_min Subset.rfl hs).antisymm subset_upperClosure

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

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

Разделы

Аффилиация

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