mem_of_not_isSuccPrelimit — Mathlib

English

If a is the least upper bound of s and a is not a succ-prelimit, then a belongs to s.

Русский

Если a является наименьшей верхней границей множества s и a не является пред-предпредлимитом, то a принадлежит s.

LaTeX

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

Lean4

theorem _root_.IsLUB.mem_of_not_isSuccPrelimit {s : Set α} (hs : IsLUB s a) (ha : ¬IsSuccPrelimit a) : a ∈ s :=
  ha.imp_symm hs.isSuccPrelimit_of_notMem

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