mem_uIoo_of_gt

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

If b < x and x < a, then x ∈ uIoo(a, b).

Русский

Если b < x и x < a, то x ∈ uIoo(a,b).

LaTeX

$$$ b < x \land x < a \Rightarrow x \in uIoo(a,b) $$$

Lean4

theorem mem_uIoo_of_gt (hb : b < x) (ha : x < a) : x ∈ uIoo a b :=
  Ioo_subset_uIoo' ⟨hb, ha⟩

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

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

Разделы

Аффилиация

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