toUpperSet

Mathlib.Topology.Sets.Order

URI: https://scilib.ai/kg/mathlib#ClopenUpperSet.toUpperSet

English

Reinterpret an upper clopen as an upper set.

Русский

Переопределение верхнего клипного множества как верхнего множества.

LaTeX

$$$\\\\operatorname{toUpperSet}(s) = \\\\langle s, s.upper \\\\rangle.$$$

Lean4

/-- Reinterpret an upper clopen as an upper set. -/
@[simps]
def toUpperSet (s : ClopenUpperSet α) : UpperSet α :=
  ⟨s, s.upper⟩

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

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

Разделы

Аффилиация

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