mem_of_not_isSuccLimit — Mathlib

English

If a is the least upper bound of s and a is not a succ-limit, then a ∈ s.

Русский

Если a является наименьшей верхней гранью s и a не является SuccLimit, то a ∈ s.

LaTeX

$$$\IsLUB(s,a) \wedge \neg \IsSuccLimit(a) \Rightarrow a \in s$$$

Lean4

theorem _root_.IsLUB.mem_of_not_isSuccLimit {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : ¬IsSuccLimit a) :
    a ∈ s :=
  ha.imp_symm <| hs.isSuccLimit_of_notMem hs'

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