interior_preimage — Mathlib

English

Let f: E → F be a surjective continuous linear map between Banach spaces. For every subset S ⊆ F, the interior of its preimage under f equals the preimage under f of the interior of S, i.e. int(f^{-1}(S)) = f^{-1}(int(S)).

Русский

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

LaTeX

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

Lean4

theorem interior_preimage (hsurj : Surjective f) (s : Set F) : interior (f ⁻¹' s) = f ⁻¹' interior s :=
  ((f.isOpenMap hsurj).preimage_interior_eq_interior_preimage f.continuous s).symm

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