isSuccLimit_of_notMem — Mathlib

English

If s has a nonempty set and a is the least upper bound of s with a ∉ s, then a is a successor-limit.

Русский

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

LaTeX

$$$\IsLUB(s,a) \wedge s \neq \varnothing \wedge a \notin s \Rightarrow \IsSuccLimit(a)$$$

Lean4

theorem _root_.IsLUB.isSuccLimit_of_notMem {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : a ∉ s) :
    IsSuccLimit a := by
  refine ⟨?_, hs.isSuccPrelimit_of_notMem ha⟩
  obtain ⟨b, hb⟩ := hs'
  obtain rfl | hb := (hs.1 hb).eq_or_lt
  · contradiction
  · exact hb.not_isMin

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