sInf_mem_closure — Mathlib

English

The infimum of a nonempty set in a space with order topology lies in the closure of the set.

Русский

На полной линейной упорядоченности с порядковой топологией наименьшее значение непустого множества принадлежит замыканию множества.

LaTeX

$$$\forall s \subseteq \alpha, s \neq \emptyset \Rightarrow sInf(s) \in \overline{s}$$$

Lean4

theorem sInf_mem_closure {s : Set α} (hs : s.Nonempty) : sInf s ∈ closure s :=
  (isGLB_sInf s).mem_closure hs

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