# 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]."

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 `ε`

.

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).