Theorems · Definition · geometry

AffineSubspace.isometryEquivMap

{𝕜 : Type u_1} →
  {V₁' : Type u_4} →
    {V₂ : Type u_5} →
      {P₁' : Type u_9} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V₁'] →
              [inst_2 : NormedSpace 𝕜 V₁'] →
                [inst_3 : MetricSpace P₁'] →
                  [inst_4 : NormedAddTorsor V₁' P₁'] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] →
                          [inst_8 : NormedAddTorsor V₂ P₂] →
                            (φ : P₁' →ᵃⁱ[𝕜] P₂) →
                              (E : AffineSubspace 𝕜 P₁') →
                                [inst_9 : Nonempty ↥E] → ↥E ≃ᵃⁱ[𝕜] ↥(AffineSubspace.map φ.toAffineMap E)

Restricts an affine isometry to an affine isometry equivalence between a nonempty affine subspace E and its image. This is an isometry version of AffineSubspace.equivMap, having a stronger premise and a stronger conclusion.

Defined in

Mathlib.Analysis.Normed.Affine.Isometry

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedFieldSeminormedAddCommGroupNormedSpaceMetricSpaceNormedAddTorsorSeminormedAddCommGroupNormedSpacePseudoMetricSpaceNormedAddTorsorNonempty