left_mem_uIcc

Mathlib.Order.Interval.Finset.Basic

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

English

The left endpoint a belongs to the upper interval [[a,b]].

Русский

Левый конец a принадлежит верхнему интервалу [[a,b]].

LaTeX

$$a \in [[a,b]]$$

Lean4

theorem left_mem_uIcc : a ∈ [[a, b]] :=
  mem_Icc.2 ⟨inf_le_left, le_sup_left⟩

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

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

Разделы

Аффилиация

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