frontier_preimage — Mathlib

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

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