csInf_Ioo

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

English

In a densely ordered lattice, for a < b, the infimum of Ioo(a,b) is a.

Русский

В плотном упорядоченном решении для a < b инфimum Ioo(a,b) равен a.

LaTeX

$$$\forall a,b:\\alpha,\ [DenselyOrdered\alpha],\ a < b \to sInf(Ioo(a,b)) = a$$$

Lean4

@[simp]
theorem csInf_Ioo [DenselyOrdered α] (h : a < b) : sInf (Ioo a b) = a :=
  (isGLB_Ioo h).csInf_eq (nonempty_Ioo.2 h)

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

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

Разделы

Аффилиация

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