mem_closure — Mathlib

English

In a linearly ordered topological space with the order topology, if a is the greatest lower bound of a nonempty set s, then a lies in the closure of s.

Русский

В линейно упорядоченном топологическом пространстве с упорядоченной топологией, если a является наибольшей нижней границей непустого множества s, то a принадлежит замыканию s.

LaTeX

$$$IsGLB\\,s\\,a \\rightarrow s \\neq \\varnothing \\rightarrow a \\in \\overline{s}$$$

Lean4

theorem mem_closure {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : a ∈ closure s :=
  (ha.frequently_nhds_mem hs).mem_closure

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