# Extending a backward bound on a normed group homomorphism from a dense set #

Possible TODO (from the PR's review, https://github.com/leanprover-community/mathlib/pull/8498 ): "This feels a lot like the second step in the proof of the Banach open mapping theorem (exists_preimage_norm_le) ... wonder if it would be possible to refactor it using one of [the lemmas in this file]."

theorem controlled_closure_of_complete {G : Type u_1} [] {H : Type u_2} {f : } {K : } {C : } {ε : } (hC : 0 < C) (hε : 0 < ε) (hyp : f.SurjectiveOnWith K C) :
f.SurjectiveOnWith K.topologicalClosure (C + ε)

Given f : NormedAddGroupHom G H for some complete G and a subgroup K of H, if every element x of K has a preimage under f whose norm is at most C*‖x‖ then the same holds for elements of the (topological) closure of K with constant C+ε instead of C, for any positive ε.

theorem controlled_closure_range_of_complete {G : Type u_1} [] {H : Type u_2} {f : } {K : Type u_3} {j : } (hj : ∀ (x : K), j x = x) {C : } {ε : } (hC : 0 < C) (hε : 0 < ε) (hyp : ∀ (k : K), ∃ (g : G), f g = j k g C * k) :
f.SurjectiveOnWith j.range.topologicalClosure (C + ε)

Given f : NormedAddGroupHom G H for some complete G, if every element x of the image of an isometric immersion j : NormedAddGroupHom K H has a preimage under f whose norm is at most C*‖x‖ then the same holds for elements of the (topological) closure of this image with constant C+ε instead of C, for any positive ε. This is useful in particular if j is the inclusion of a normed group into its completion (in this case the closure is the full target group).