English
Let f: E → F be a surjective continuous linear map between Banach spaces. For any subset S ⊆ F, the boundary satisfies: frontier(f^{-1}(S)) = f^{-1}(frontier(S)).
Русский
Пусть f: E → F — сюръективное непрерывное линейное отображение между банаховыми пространствами. Граница выполняется как frontier(f^{-1}(S)) = f^{-1}(frontier(S)).
LaTeX
$$$\\partial(f^{-1}(S)) = f^{-1}(\\partial S)$$$
Lean4
theorem frontier_preimage (hsurj : Surjective f) (s : Set F) : frontier (f ⁻¹' s) = f ⁻¹' frontier s :=
((f.isOpenMap hsurj).preimage_frontier_eq_frontier_preimage f.continuous s).symm