isPredLimit_of_notMem — Mathlib

English

If a is the greatest lower bound of a nonempty set s and a ∉ s, then a is a predecessor limit.

Русский

Если a — наибольшая нижняя грань множества s и a∉s, тогда a является пределом предшественника.

LaTeX

$$$IsGLB\ s\ a \wedge s \neq \varnothing \wedge a \notin s \Rightarrow IsPredLimit\ a$$$

Lean4

theorem _root_.IsGLB.isPredLimit_of_notMem {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) (ha : a ∉ s) :
    IsPredLimit a := by simpa using (IsGLB.dual hs).isSuccLimit_of_notMem hs' ha

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