isSuccPrelimit_of_notMem — Mathlib

English

Let s be a subset of a linear order α and let a be the least upper bound of s with a ∉ s. Then a is a successor-prelimit of s, i.e., for every b < a there exists c ∈ s with b < c ≤ a.

Русский

Пусть s ⊆ α и a = sup s, причём a ∉ s. Тогда a является предпределителем-последователем множества s: для каждого b < a существует c ∈ s такое, что b < c ≤ a.

LaTeX

$$$\IsLUB(s,a) \wedge a \notin s \Rightarrow \IsSuccPrelimit(a)$$$

Lean4

theorem _root_.IsLUB.isSuccPrelimit_of_notMem {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) : IsSuccPrelimit a :=
  by
  intro b hb
  obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt
  obtain rfl := (hb.ge_of_gt hbc).antisymm hca
  contradiction

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