csInf_Ioc

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#csInf_Ioc

English

The infimum of the closed interval Icc(a,b) equals a when a ≤ b.

Русский

Infimum закрытого интервала Icc(a,b) равен a при a ≤ b.

LaTeX

$$$\forall a,b:\\alpha,\ a \le b \to sInf(Icc(a,b)) = a$$$

Lean4

@[simp]
theorem csInf_Ioc [DenselyOrdered α] (h : a < b) : sInf (Ioc a b) = a :=
  (isGLB_Ioc h).csInf_eq (nonempty_Ioc.2 h)

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

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

Разделы

Аффилиация

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