isPredPrelimit_of_notMem — Mathlib

English

If s has IsGLB at a and a ∉ s, then a is a pred-prelimit.

Русский

Если множество s имеет GLB в точке a, и a не принадлежит s, то a является пред-предпредельным.

LaTeX

$$$IsGLB\\ s\\ a \\to a \\notin s \\to IsPredPrelimit\\ a$$$

Lean4

theorem _root_.IsGLB.isPredPrelimit_of_notMem {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) : IsPredPrelimit a := by
  simpa using (IsGLB.dual hs).isSuccPrelimit_of_notMem ha

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