mem_of_nonempty_of_not_isSuccPrelimit

English

Let s be a nonempty subset with x a least upper bound. If x is not a succ-prelimit, then x ∈ s.

Русский

Пусть s — непустое множество и x — наименьшая верхняя грань множества. Если x не является succ-предельным пределом, то x принадлежит s.

LaTeX

$$$ IsLUB\\, s\\, x \\rightarrow s \\neq \\varnothing \\rightarrow \\neg IsSuccPrelimit x \\rightarrow x \\in s $$$

Lean4

theorem mem_of_nonempty_of_not_isSuccPrelimit (hs : IsLUB s x) (hne : s.Nonempty) (hx : ¬IsSuccPrelimit x) : x ∈ s :=
  hs.csSup_eq hne ▸ csSup_mem_of_not_isSuccPrelimit hne hs.bddAbove (hs.csSup_eq hne ▸ hx)

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