isOpen_Ico_zero

Mathlib.Topology.Instances.NNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#NNReal.isOpen_Ico_zero

English

For every x in NNReal, the half-open interval [0, x) is open in NNReal.

Русский

Для любого x в NNReal полупрерывный интервал [0, x) открыт в NNReal.

LaTeX

$$$IsOpen(\\mathrm{Ico}(0,x))$$$

Lean4

theorem isOpen_Ico_zero {x : NNReal} : IsOpen (Set.Ico 0 x) :=
  Ico_bot (a := x) ▸ isOpen_Iio

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

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

Разделы

Аффилиация

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