of_closure — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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