Theorems · Definition · functional analysis

IsometryEquiv.vaddConst

{V : Type u_2} →
  {P : Type u_3} →
    [inst : SeminormedAddCommGroup V] → [inst_1 : PseudoMetricSpace P] → [NormedAddTorsor V P] → P → V ≃ᵢ P

Isometry between the tangent space V of a (semi)normed add torsor P and P given by addition/subtraction of x : P.

Defined in

Mathlib.Analysis.Normed.Group.AddTorsor

Cited by

14 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupPseudoMetricSpaceNormedAddTorsor