mem_Iio

Mathlib.Order.Interval.Multiset

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

English

x ∈ Iio(b) iff x < b.

Русский

x ∈ Iio(b) тогда и только тогда, когда x < b.

LaTeX

$$$x \in \mathrm{Iio}(b) \iff x < b$$$

Lean4

@[simp]
theorem mem_Iio : x ∈ Iio b ↔ x < b := by rw [Iio, ← Finset.mem_def, Finset.mem_Iio]

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

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

Разделы

Аффилиация

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