Theorems · Definition · functional analysis

NormedGroup.induced

{𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : Group E] →
          [inst_2 : NormedGroup F] → [MonoidHomClass 𝓕 E F] → (f : 𝓕) → Function.Injective ⇑f → NormedGroup E

An injective group homomorphism from a Group to a NormedGroup induces a NormedGroup structure on the domain.

Defined in

Mathlib.Analysis.Normed.Group.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeGroupNormedGroupMonoidHomClass