closure_image_closure — Mathlib

English

For a continuous map f, the closure of the image of closure s equals the closure of the image of s.

Русский

Замыкание образа замыкания множества равно замыканию образа множества.

LaTeX

$$$\\overline{f[\\overline{s}]} = \\overline{f[s]} \\quad \\text{for } f \\text{ continuous}$$$

Lean4

theorem closure_image_closure (h : Continuous f) : closure (f '' closure s) = closure (f '' s) :=
  Subset.antisymm (closure_minimal (image_closure_subset_closure_image h) isClosed_closure)
    (closure_mono <| image_mono subset_closure)

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