closure_preimage — Mathlib

English

Let f: E → F be a surjective continuous linear map between Banach spaces. For any subset S ⊆ F, the closure of its preimage equals the preimage of the closure: cl(f^{-1}(S)) = f^{-1}(cl(S)).

Русский

Пусть f: E → F — сюръективное непрерывное линейное отображение между банаховыми пространствами. Тогда замыкание прообраза равно прообраз замыкания: cl(f^{-1}(S)) = f^{-1}(cl(S)).

LaTeX

$$$\\operatorname{cl}(f^{-1}(S)) = f^{-1}(\\operatorname{cl}(S))$$$

Lean4

theorem closure_preimage (hsurj : Surjective f) (s : Set F) : closure (f ⁻¹' s) = f ⁻¹' closure s :=
  ((f.isOpenMap hsurj).preimage_closure_eq_closure_preimage f.continuous s).symm

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