Theorems · Definition · functional analysis

NormedAddGroupHom.SurjectiveOnWith

{V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] →
      [inst_1 : SeminormedAddCommGroup V₂] → NormedAddGroupHom V₁ V₂ → AddSubgroup V₂ → ℝ → Prop

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.

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

6 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup