sSup_mem_of_not_isSuccPrelimit — Mathlib

English

In a complete linear order, if s is a set and sSup s is not a succ-prelimit, then sSup s lies in s.

Русский

В полном линейном порядке, если s — множество и sSup s не является succ-пред пределом, то sSup s принадлежит s.

LaTeX

$$$ \\forall s:\\ Set\\; \\neg IsSuccPrelimit (sSup s) \\Rightarrow sSup s \\in s $$$

Lean4

theorem sSup_mem_of_not_isSuccPrelimit (hlim : ¬IsSuccPrelimit (sSup s)) : sSup s ∈ s :=
  by
  obtain ⟨y, hy⟩ := not_forall_not.mp hlim
  obtain ⟨i, his, hi⟩ := lt_sSup_iff.mp hy.lt
  exact eq_of_le_of_not_lt (le_sSup his) (hy.2 hi) ▸ his

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