isLUB_of_mem_closure — Mathlib

English

If a is the greatest lower bound of s and a is in the closure of s, then a is the greatest lower bound of s.

Русский

Если a является наибольшей нижней границей s и лежит в замыкании s, то a является наибольшей нижней границей s.

LaTeX

$$$a\\in upperBounds s \\land a\\in closure s \\Rightarrow IsLUB s a$$$

Lean4

theorem isLUB_of_mem_closure {s : Set α} {a : α} (hsa : a ∈ upperBounds s) (hsf : a ∈ closure s) : IsLUB s a :=
  by
  rw [mem_closure_iff_clusterPt, ClusterPt, inf_comm] at hsf
  exact isLUB_of_mem_nhds hsa (mem_principal_self s)

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