isGLB_csInf

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

English

If s is nonempty and bounded below, then IsGLB s (sInf s).

Русский

Если s непусто и ограничено снизу, то sInf s является наибольшей меньшей гранью множества s.

LaTeX

$$$s \neq \varnothing \land BddBelow(s) \rightarrow IsGLB(s, \mathrm{sInf}(s))$$$

Lean4

theorem isGLB_csInf (ne : s.Nonempty) (H : BddBelow s) : IsGLB s (sInf s) :=
  ⟨fun _ => csInf_le H, fun _ => le_csInf ne⟩

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

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

Разделы

Аффилиация

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