csSup_mem_of_not_isSuccPrelimit' — Mathlib

English

Let s be a set and assume s is bounded above. If sSup s is not a succ-prelimit, then sSup s ∈ s.

Русский

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

LaTeX

$$$ BddAbove\\, s \\to \\neg IsSuccPrelimit (sSup s) \\Rightarrow sSup s \\in s $$$

Lean4

/-- See `csSup_mem_of_not_isSuccPrelimit` for the `ConditionallyCompleteLinearOrder` version. -/
theorem csSup_mem_of_not_isSuccPrelimit' (hbdd : BddAbove s) (hlim : ¬IsSuccPrelimit (sSup s)) : sSup s ∈ s :=
  by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [isSuccPrelimit_bot] at hlim
  · exact csSup_mem_of_not_isSuccPrelimit hs hbdd hlim

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