mem_Ioo

Mathlib.Order.Interval.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.mem_Ioo

English

For a < x < b, x belongs to Ioo(a,b); otherwise it does not.

Русский

Элемент x принадлежит Ioo(a,b) тогда и только тогда, когда a < x и x < b.

LaTeX

$$$x \in \mathrm{Ioo}(a,b) \iff a < x \land x < b$$$

Lean4

@[simp]
theorem mem_Ioo : x ∈ Ioo a b ↔ a < x ∧ x < b := by rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]

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

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

Разделы

Аффилиация

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