compl_Iic

Mathlib.Order.Interval.Set.LinearOrder

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

English

The complement of the closed ray [a, ∞) is the open ray (−∞, a).

Русский

Комплемент непрерывного луча [a, ∞) равен открытому лучу (−∞, a).

LaTeX

$$$(\\{x \\mid x \\ge a\\})^{c} = \\{x \\mid x < a\\}$$$

Lean4

@[simp]
theorem compl_Iic : (Iic a)ᶜ = Ioi a :=
  ext fun _ => not_le

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

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

Разделы

Аффилиация

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