English
Open mapping theorem specialized form using continuous linear maps reduces to the standard open mapping theorem.
Русский
Специализированная форма теоремы об открытом отображении для линейных отображений сводится к стандартной теореме об открытом отображении.
LaTeX
$$$$\\text{IsOpenMap}(f)$$$$
Lean4
/-- The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is
open. -/
protected theorem isOpenMap (surj : Surjective f) : IsOpenMap f :=
by
intro s hs
rcases exists_preimage_norm_le f surj with ⟨C, Cpos, hC⟩
refine isOpen_iff.2 fun y yfs => ?_
rcases yfs with ⟨x, xs, fxy⟩
rcases isOpen_iff.1 hs x xs with ⟨ε, εpos, hε⟩
refine ⟨ε / C, div_pos εpos Cpos, fun z hz => ?_⟩
rcases hC (z - y) with ⟨w, wim, wnorm⟩
have : f (x + w) = z := by rw [f.map_add, wim, fxy, add_sub_cancel]
rw [← this]
have : x + w ∈ ball x ε :=
calc
dist (x + w) x = ‖w‖ := by simp
_ ≤ C * ‖z - y‖ := wnorm
_ < C * (ε / C) := by
apply mul_lt_mul_of_pos_left _ Cpos
rwa [mem_ball, dist_eq_norm] at hz
_ = ε := mul_div_cancel₀ _ (ne_of_gt Cpos)
exact Set.mem_image_of_mem _ (hε this)
