closure_lowerClosure_comm_pi — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem closure_lowerClosure_comm_pi (hs : BddAbove s) :
    closure (lowerClosure s : Set (ι → ℝ)) = lowerClosure (closure s) :=
  (closure_minimal (lowerClosure_mono subset_closure) <| isClosed_closure.lowerClosure_pi hs.closure).antisymm <|
    lowerClosure_min (closure_mono subset_lowerClosure) (lowerClosure s).lower.closure

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