isGLB_of_mem_closure — Mathlib

English

In a linearly ordered topological space with the order topology, if a is the greatest lower bound of s and a ∈ closure s, then a is the GLB of s.

Русский

В линейно упорядоченном топологическом пространстве с упорядоченной топологией, если a является наибольшей нижней границей s и a ∈ closure(s), то a является ГЛБ s.

LaTeX

$$$a\\in lowerBounds s \\land a\\in closure s \\Rightarrow IsGLB s a$$$

Lean4

theorem isGLB_of_mem_closure {s : Set α} {a : α} (hsa : a ∈ lowerBounds s) (hsf : a ∈ closure s) : IsGLB s a :=
  isLUB_of_mem_closure (α := αᵒᵈ) hsa hsf

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