isOpen_ofUpperSet_preimage

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithUpperSet.isOpen_ofUpperSet_preimage

English

For subsets s of α, IsOpen (ofUpperSet⁻¹' s) iff IsUpperSet s.

Русский

Для подмножеств s пространства α IsOpen(ofUpperSet⁻¹' s) эквивалентно IsUpperSet s.

LaTeX

$$$IsOpen(\\mathrm{ofUpperSet}^{-1}(s)) \\iff IsUpperSet(s).$$$

Lean4

@[simp]
theorem isOpen_ofUpperSet_preimage {s : Set α} : IsOpen (ofUpperSet ⁻¹' s) ↔ IsUpperSet s :=
  isUpperSet_toUpperSet_preimage.symm

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

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

Разделы

Аффилиация

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