Ioi_ssubset_Ici_self

Mathlib.Order.Interval.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.Ioi_ssubset_Ici_self

English

The open interval (a, ∞) is strictly contained in the closed interval [a, ∞). In symbols: Ioi(a) ⊂ Ici(a).

Русский

Открытый интервал (a, ∞) вложен строго в закрытый интервал [a, ∞). То есть Ioi(a) ⊂ Ici(a).

LaTeX

$$$$Ioi(a) \subsetneq Ici(a)$$$$

Lean4

theorem Ioi_ssubset_Ici_self : Ioi a ⊂ Ici a :=
  ⟨Ioi_subset_Ici_self, fun h => lt_irrefl a (h le_rfl)⟩

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

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

Разделы

Аффилиация

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