notMem_Iic

Mathlib.Order.Interval.Set.LinearOrder

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

English

For any a,b in a linear order, c ∉ [−∞, b] iff b < c.

Русский

Для любых a,b в линейном порядке: c не лежит в [−∞, b] тогда и только тогда, когда b < c.

LaTeX

$$$c \\notin (-\\infty, b] \\iff b < c$$$

Lean4

theorem notMem_Iic : c ∉ Iic b ↔ b < c :=
  not_le

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

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

Разделы

Аффилиация

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