mem_Iio

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.mem_Iio

English

Characterization of membership in Iio: x ∈ Iio(a) if and only if x < a.

Русский

Принадлежность x к Iio: x принадлежит тогда и только тогда, когда x < a.

LaTeX

$$$x \in Iio(a) \;\iff\; x < a$$$

Lean4

@[simp]
theorem mem_Iio : x ∈ Iio a ↔ x < a :=
  LocallyFiniteOrderBot.finset_mem_Iio _ _

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

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

Разделы

Аффилиация

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