mem_Ioc

Mathlib.Order.Interval.Finset.Defs

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

English

Membership in Ioc is equivalent to a < x and x ≤ b.

Русский

Членство в Ioc эквивалентно a < x и x ≤ b.

LaTeX

$$$x \in Ioc(a,b) \iff a < x \land x \le b$$$

Lean4

@[simp]
theorem mem_Ioc : x ∈ Ioc a b ↔ a < x ∧ x ≤ b :=
  LocallyFiniteOrder.finset_mem_Ioc a b x

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

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

Разделы

Аффилиация

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