upperClosure

Mathlib.Topology.Algebra.Order.UpperLower

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

English

If s is open, then the upperClosure of s is open.

Русский

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

LaTeX

$$$IsOpen\\;s \\Rightarrow IsOpen(UpperClosure\\;s)$$$

Lean4

protected theorem upperClosure : IsOpen s → IsOpen (upperClosure s : Set α) :=
  HasUpperLowerClosure.isOpen_upperClosure _

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

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

Разделы

Аффилиация

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