csSup_mem_of_not_isSuccPrelimit — Mathlib

English

In a ConditionallyCompleteLinearOrder, if s is nonempty, bounded above, and its supremum is not a succ-prelimit, then the supremum belongs to s.

Русский

В условно-завершенном линейном порядке, если s непусто, ограничено сверху, и верхняя граница не является предельной точкой, то s содержит sup s.

LaTeX

$$$$ s.Nonempty \rightarrow BddAbove s \rightarrow \neg IsSuccPrelimit (sSup s) \rightarrow sSup s \in s $$$$

Lean4

theorem csSup_mem_of_not_isSuccPrelimit (hne : s.Nonempty) (hbdd : BddAbove s) (hlim : ¬IsSuccPrelimit (sSup s)) :
    sSup s ∈ s := by
  obtain ⟨y, hy⟩ := not_forall_not.mp hlim
  obtain ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt
  exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his

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