preimage_closure_eq_closure_preimage

English

If f is open and continuous, then the preimage of the closure equals the closure of the preimage.

Русский

Если f открытое и непрерывное отображение, то f^{-1}(closure s) = closure(f^{-1}(s)).

LaTeX

$$$$IsOpenMap(f) \\land Continuous(f) \\rightarrow \\forall s, f^{-1}(\\mathrm{closure}(s)) = \\mathrm{closure}(f^{-1}(s))$$$$

Lean4

theorem preimage_closure_eq_closure_preimage (hf : IsOpenMap f) (hfc : Continuous f) (s : Set Y) :
    f ⁻¹' closure s = closure (f ⁻¹' s) :=
  hf.preimage_closure_subset_closure_preimage.antisymm (hfc.closure_preimage_subset s)

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