isOpen_Ico_zero

Mathlib.Topology.Instances.ENNReal.Lemmas

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

English

For any b ∈ ENNReal, the half-open interval Ico(0,b) is open in ENNReal.

Русский

Для любого b ∈ ℝ≥0∞ полуинтервал Ico(0,b) открыт в ENNReal.

LaTeX

$$$\\operatorname{IsOpen}(\\mathrm{Ico}(0,b))$$$

Lean4

theorem isOpen_Ico_zero : IsOpen (Ico 0 b) := by
  rw [ENNReal.Ico_eq_Iio]
  exact isOpen_Iio

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

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

Разделы

Аффилиация

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