notMem_Ici

Mathlib.Order.Interval.Set.LinearOrder

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

English

For any a in a linear order, c ∉ [a, ∞) if and only if c < a.

Русский

Для любого a в линейном порядке верно, что c не принадлежит [a, ∞) тогда и только тогда, когда c < a.

LaTeX

$$$c \\notin [a, \\infty) \\iff c < a$$$

Lean4

theorem notMem_Ici : c ∉ Ici a ↔ c < a :=
  not_le

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

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

Разделы

Аффилиация

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