mem_of_nonempty_of_not_isPredPrelimit

English

Let s be a nonempty subset with x the greatest lower bound. If x is not a pred-prelimit, then x ∈ s.

Русский

Пусть s — непустое множество и x — наибольший нижний предел множества. Если x не является pred-пределом, то x принадлежит s.

LaTeX

$$$ IsGLB\\, s\\, x \\rightarrow s.Nonempty \\rightarrow \\neg IsPredPrelimit x \\rightarrow x \\in s $$$

Lean4

theorem mem_of_nonempty_of_not_isPredPrelimit (hs : IsGLB s x) (hne : s.Nonempty) (hx : ¬IsPredPrelimit x) : x ∈ s :=
  hs.csInf_eq hne ▸ csInf_mem_of_not_isPredPrelimit hne hs.bddBelow (hs.csInf_eq hne ▸ hx)

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