left_mem_Ioo

Mathlib.Order.Interval.Set.Basic

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

English

The left endpoint is not contained in the open interval: a ∈ Ioo(a,b) is false.

Русский

Левый пункт не принадлежит открытому интервалу: a ∈ Ioo(a,b) ложно.

LaTeX

$$$ a \in Ioo(a,b) \iff False $$$

Lean4

theorem left_mem_Ioo : a ∈ Ioo a b ↔ False := by simp

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

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

Разделы

Аффилиация

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