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)