isGLB_Ioi

Mathlib.Order.Bounds.Basic

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

English

In a densely ordered linear order, the greatest lower bound of Ioi(a) is a, for any a ∈ γ.

Русский

В плотном линейном порядке наибольшая нижняя граница множества Ioi(a) равна a для любого a.

LaTeX

$$$ IsGLB(Ioi(a))\ a. $$$

Lean4

theorem isGLB_Ioi {a : γ} : IsGLB (Ioi a) a :=
  @isLUB_Iio γᵒᵈ _ _ a

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

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

Разделы

Аффилиация

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