lowerClosure

Mathlib.Topology.Algebra.Order.UpperLower

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

English

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

Русский

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

LaTeX

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

Lean4

protected theorem lowerClosure : IsOpen s → IsOpen (lowerClosure s : Set α) :=
  HasUpperLowerClosure.isOpen_lowerClosure _

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

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

Разделы

Аффилиация

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