closure_upperClosure_comm_pi — Mathlib

English

For a bounded-below subset s of ℝ^ι, the closure of its upperClosure equals the upperClosure of its closure.

Русский

Для ограниченного снизу множества s ⊆ ℝ^ι замыкание верхней окрестности совпадает с верхней окрестностью замыкания: cl(upperClosure(s)) = upperClosure(cl(s)).

LaTeX

$$$\mathrm{closure}(\mathrm{upperClosure}(s)) = \mathrm{upperClosure}(\mathrm{closure}(s)).$$$

Lean4

theorem closure_upperClosure_comm_pi (hs : BddBelow s) :
    closure (upperClosure s : Set (ι → ℝ)) = upperClosure (closure s) :=
  (closure_minimal (upperClosure_anti subset_closure) <| isClosed_closure.upperClosure_pi hs.closure).antisymm <|
    upperClosure_min (closure_mono subset_upperClosure) (upperClosure s).upper.closure

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