isGLB_sInf — Mathlib

English

For a ConditionallyCompleteLattice β, any bounded-below s ⊆ WithTop β has IsGLB s (sInf s).

Русский

Для условно полноупорядоченной решетки β любой ограниченно снизу множество s ⊆ WithTop β имеет IsGLB s (sInf s).

LaTeX

$$$\text{BddBelow}(s) \Rightarrow IsGLB(s, sInf(s))$$$

Lean4

theorem isGLB_sInf (s : Set (WithTop α)) : IsGLB s (sInf s) :=
  by
  by_cases hs : BddBelow s
  · exact isGLB_sInf' hs
  · exfalso
    apply hs
    use ⊥
    intro _ _
    exact bot_le

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