mem_of_not_isPredLimit — Mathlib

English

If IsGLB(s,a) and s is nonempty and a is not a pred-limit, then a ∈ s.

Русский

Если IsGLB(s,a) и s непусто и a не является пред-предельным, тогда a ∈ s.

LaTeX

$$IsGLB\\ s\\ a \\to s.Nonempty \\to (Not IsPredLimit\\ a) \\to a \\in s$$

Lean4

theorem _root_.IsGLB.mem_of_not_isPredLimit {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) (ha : ¬IsPredLimit a) :
    a ∈ s :=
  ha.imp_symm <| hs.isPredLimit_of_notMem hs'

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