notMem_Ioi

Mathlib.Order.Interval.Set.LinearOrder

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

English

For any a, c ∉ (a, ∞) if and only if c ≤ a.

Русский

Для любого a и c: c не принадлежит (a, ∞) тогда и только тогда, когда c ≤ a.

LaTeX

$$$c \\notin (a, \\infty) \\iff c \\le a$$$

Lean4

theorem notMem_Ioi : c ∉ Ioi a ↔ c ≤ a :=
  not_lt

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

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

Разделы

Аффилиация

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