English
A normed additive group morphism is surjective on a subgroup K with a bound C if every element of K has a preimage whose norm is at most C times the preimage’s norm.
Русский
Гомоморфизм нормированной аддитивной группы сюръективен на подгруппе K с константой C, если каждый элемент K имеет предобраз с нормой не большей C⋅норма(предобраза).
LaTeX
$$$\\text{SurjectiveOnWith}(f,K,C):\\; ∀ h\\in K, \\exists g, f(g)=h ∧ ‖g‖ ≤ C·‖h‖$$$
Lean4
/-- A normed group hom is surjective on the subgroup `K` with constant `C` if every element
`x` of `K` has a preimage whose norm is bounded above by `C*‖x‖`. This is a more
abstract version of `f` having a right inverse defined on `K` with operator norm
at most `C`. -/
def SurjectiveOnWith (f : NormedAddGroupHom V₁ V₂) (K : AddSubgroup V₂) (C : ℝ) : Prop :=
∀ h ∈ K, ∃ g, f g = h ∧ ‖g‖ ≤ C * ‖h‖
