of_closure — Mathlib

English

Let α be a preorder space with a topology. For any subset s ⊆ α, if the closure of s is bounded below, then s is bounded below.

Русский

Пусть α — пространство с порядком и топологией. Для любого s ⊆ α, если замыкание s ограничено снизу, то и s ограничено снизу.

LaTeX

$$$\operatorname{BddBelow}(\overline{s}) \Rightarrow \operatorname{BddBelow}(s)$$$

Lean4

protected theorem of_closure : BddBelow (closure s) → BddBelow s :=
  BddBelow.mono subset_closure

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