Theorems · Definition · functional analysis

AffineIsometry.toAffineIsometryEquiv

{𝕜 : Type u_1} →
  {V₁ : Type u_2} →
    {V₂ : Type u_3} →
      {P₁ : Type u_4} →
        {P₂ : Type u_5} →
          [inst : NormedField 𝕜] →
            [inst_1 : NormedAddCommGroup V₁] →
              [inst_2 : SeminormedAddCommGroup V₂] →
                [inst_3 : NormedSpace 𝕜 V₁] →
                  [inst_4 : NormedSpace 𝕜 V₂] →
                    [inst_5 : MetricSpace P₁] →
                      [inst_6 : PseudoMetricSpace P₂] →
                        [inst_7 : NormedAddTorsor V₁ P₁] →
                          [inst_8 : NormedAddTorsor V₂ P₂] →
                            [FiniteDimensional 𝕜 V₁] →
                              [FiniteDimensional 𝕜 V₂] →
                                [Inhabited P₁] →
                                  (P₁ →ᵃⁱ[𝕜] P₂) → Module.finrank 𝕜 V₁ = Module.finrank 𝕜 V₂ → P₁ ≃ᵃⁱ[𝕜] P₂

An affine isometry between finite-dimensional spaces of equal dimension can be upgraded to an affine isometry equivalence.

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedAddCommGroupSeminormedAddCommGroupNormedSpaceNormedSpaceMetricSpacePseudoMetricSpaceNormedAddTorsorNormedAddTorsorFiniteDimensionalFiniteDimensionalInhabited