isUpperSet_of_isClosed

Mathlib.Topology.Order.LowerUpperTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsLower.isUpperSet_of_isClosed

English

If s is closed, then s is an upper set.

Русский

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

LaTeX

$$$\\text{IsClosed}(s) \\Rightarrow \\text{IsUpperSet}(s)$$$

Lean4

theorem isUpperSet_of_isClosed (h : IsClosed s) : IsUpperSet s :=
  isLowerSet_compl.1 <| isLowerSet_of_isOpen h.isOpen_compl

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

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

Разделы

Аффилиация

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