instConditionallyCompleteLinearOrder

English

If s is nonempty and bounded above, there exists x with IsLUB s x.

Русский

Если s непусто и ограничено сверху, существует such x, который является наименьшей верхней гранью множества.

LaTeX

$$$\exists x\, IsLUB(s,x)$$$

Lean4

noncomputable instance : ConditionallyCompleteLinearOrder ℝ
    where
  __ := Real.linearOrder
  __ := Real.lattice
  le_csSup s a hs ha := (Real.isLUB_sSup ⟨a, ha⟩ hs).1 ha
  csSup_le s a hs ha := (Real.isLUB_sSup hs ⟨a, ha⟩).2 ha
  csInf_le s a hs ha := (Real.isGLB_sInf ⟨a, ha⟩ hs).1 ha
  le_csInf s a hs ha := (Real.isGLB_sInf hs ⟨a, ha⟩).2 ha
  csSup_of_not_bddAbove s hs := by simp [hs, sSup_def]
  csInf_of_not_bddBelow s hs := by simp [hs, sInf_def, sSup_def]

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