closure_preimage_subset — Mathlib

English

For a continuous map f, closure of the preimage is contained in the preimage of the closure.

Русский

Для непрерывного отображения f замыкание предобраза содержится в предобразе замыкания.

LaTeX

$$$\\operatorname{closure}(f^{-1}(t)) \\subseteq f^{-1}(\\operatorname{closure}(t))$$$

Lean4

theorem closure_preimage_subset (hf : Continuous f) (t : Set Y) : closure (f ⁻¹' t) ⊆ f ⁻¹' closure t :=
  by
  rw [← (isClosed_closure.preimage hf).closure_eq]
  exact closure_mono (preimage_mono subset_closure)

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