mem_Ioi

Mathlib.Order.Interval.Set.Defs

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

English

For all x in α, x belongs to Ioi(a) if and only if a < x.

Русский

Для всех x в α выполняется: x ∈ Ioi(a) тогда и только тогда, когда a < x.

LaTeX

$$$$ x \in Ioi(a) \iff a < x. $$$$

Lean4

@[simp, grind =]
theorem mem_Ioi : x ∈ Ioi a ↔ a < x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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