isOpen_Iio'

Mathlib.Topology.Order.Basic

URI: https://scilib.ai/kg/mathlib#isOpen_Iio'

English

In an OrderTopology α, Iio(a) is open for any a; equivalently, Iio(a) = Ioi(a) under duality.

Русский

Для каждого a множество Iio(a) открыто; эквивалентно Iio(a) равняется Ioi(a) при двойственности.

LaTeX

$$$\\text{IsOpen}(Iio(a))$$$

Lean4

theorem isOpen_Iio' [OrderTopology α] (a : α) : IsOpen (Iio a) :=
  isOpen_gt' a

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

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

Разделы

Аффилиация

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