Theorems · Definition · geometry

AffineSubspace.equivMapOfInjective

{𝕜 : Type u_1} →
  {V₁ : Type u_3} →
    {V₂ : Type u_5} →
      {P₁ : Type u_8} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V₁] →
              [inst_2 : NormedSpace 𝕜 V₁] →
                [inst_3 : PseudoMetricSpace P₁] →
                  [inst_4 : NormedAddTorsor V₁ P₁] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] →
                          [inst_8 : NormedAddTorsor V₂ P₂] →
                            (E : AffineSubspace 𝕜 P₁) →
                              [inst_9 : Nonempty ↥E] →
                                (φ : P₁ →ᵃ[𝕜] P₂) → Function.Injective ⇑φ → ↥E ≃ᵃ[𝕜] ↥(AffineSubspace.map φ E)

An affine subspace is isomorphic to its image under an injective affine map. This is the affine version of Submodule.equivMapOfInjective.

Defined in

Mathlib.Analysis.Normed.Affine.Isometry

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedFieldSeminormedAddCommGroupNormedSpacePseudoMetricSpaceNormedAddTorsorSeminormedAddCommGroupNormedSpacePseudoMetricSpaceNormedAddTorsorNonempty