Documentation

Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv

Continuous affine equivalences #

In this file, we define continuous affine equivalences, affine equivalences which are continuous with continuous inverse.

Main definitions #

TODO #

structure ContinuousAffineEquiv (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_4} {V₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] extends AffineEquiv :
Type (max (max (max u_2 u_3) u_4) u_5)

A continuous affine equivalence, denoted P₁ ≃ᵃL[k] P₂, between two affine topological spaces is an affine equivalence such that forward and inverse maps are continuous.

  • toFun : P₁P₂
  • invFun : P₂P₁
  • left_inv : Function.LeftInverse (self).invFun (self).toFun
  • right_inv : Function.RightInverse (self).invFun (self).toFun
  • linear : V₁ ≃ₗ[k] V₂
  • map_vadd' : ∀ (p : P₁) (v : V₁), (self).toEquiv (v +ᵥ p) = (self).linear v +ᵥ (self).toEquiv p
  • continuous_toFun : Continuous (self).toFun
  • continuous_invFun : Continuous (self).invFun
Instances For
    theorem ContinuousAffineEquiv.continuous_toFun {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (self : P₁ ≃ᵃL[k] P₂) :
    Continuous (self).toFun
    theorem ContinuousAffineEquiv.continuous_invFun {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] (self : P₁ ≃ᵃL[k] P₂) :
    Continuous (self).invFun

    A continuous affine equivalence, denoted P₁ ≃ᵃL[k] P₂, between two affine topological spaces is an affine equivalence such that forward and inverse maps are continuous.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def ContinuousAffineEquiv.toHomeomorph {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
      P₁ ≃ₜ P₂

      A continuous affine equivalence is a homeomorphism.

      Equations
      • e.toHomeomorph = let __spread.0 := e; { toEquiv := (__spread.0).toEquiv, continuous_toFun := , continuous_invFun := }
      Instances For
        theorem ContinuousAffineEquiv.toAffineEquiv_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] :
        Function.Injective ContinuousAffineEquiv.toAffineEquiv
        instance ContinuousAffineEquiv.instEquivLike {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] :
        EquivLike (P₁ ≃ᵃL[k] P₂) P₁ P₂
        Equations
        • ContinuousAffineEquiv.instEquivLike = { coe := fun (f : P₁ ≃ᵃL[k] P₂) => (f).toFun, inv := fun (f : P₁ ≃ᵃL[k] P₂) => (f).invFun, left_inv := , right_inv := , coe_injective' := }
        instance ContinuousAffineEquiv.instCoeFunForall {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] :
        CoeFun (P₁ ≃ᵃL[k] P₂) fun (x : P₁ ≃ᵃL[k] P₂) => P₁P₂
        Equations
        • ContinuousAffineEquiv.instCoeFunForall = DFunLike.hasCoeToFun
        instance ContinuousAffineEquiv.coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] :
        Coe (P₁ ≃ᵃL[k] P₂) (P₁ ≃ᵃ[k] P₂)

        Coerce continuous affine equivalences to affine equivalences.

        Equations
        • ContinuousAffineEquiv.coe = { coe := ContinuousAffineEquiv.toAffineEquiv }
        theorem ContinuousAffineEquiv.coe_injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] :
        Function.Injective ContinuousAffineEquiv.toAffineEquiv
        instance ContinuousAffineEquiv.instFunLike {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] :
        FunLike (P₁ ≃ᵃL[k] P₂) P₁ P₂
        Equations
        • ContinuousAffineEquiv.instFunLike = { coe := fun (f : P₁ ≃ᵃL[k] P₂) => f, coe_injective' := }
        @[simp]
        theorem ContinuousAffineEquiv.coe_coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
        e = e
        @[simp]
        theorem ContinuousAffineEquiv.coe_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
        (e).toEquiv = e
        def ContinuousAffineEquiv.Simps.apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
        P₁P₂

        See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

        Equations
        Instances For
          def ContinuousAffineEquiv.Simps.coe {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
          P₁ ≃ᵃ[k] P₂

          See Note [custom simps projection].

          Equations
          Instances For
            theorem ContinuousAffineEquiv.ext {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] {e : P₁ ≃ᵃL[k] P₂} {e' : P₁ ≃ᵃL[k] P₂} (h : ∀ (x : P₁), e x = e' x) :
            e = e'
            theorem ContinuousAffineEquiv.ext_iff {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] {e : P₁ ≃ᵃL[k] P₂} {e' : P₁ ≃ᵃL[k] P₂} :
            e = e' ∀ (x : P₁), e x = e' x
            theorem ContinuousAffineEquiv.continuous {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
            def ContinuousAffineEquiv.refl (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] :
            P₁ ≃ᵃL[k] P₁

            Identity map as a ContinuousAffineEquiv.

            Equations
            Instances For
              @[simp]
              theorem ContinuousAffineEquiv.coe_refl {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] :
              @[simp]
              theorem ContinuousAffineEquiv.refl_apply {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] (x : P₁) :
              @[simp]
              theorem ContinuousAffineEquiv.toAffineEquiv_refl {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] :
              @[simp]
              theorem ContinuousAffineEquiv.toEquiv_refl {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] :
              ((ContinuousAffineEquiv.refl k P₁)).toEquiv = Equiv.refl P₁
              def ContinuousAffineEquiv.symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
              P₂ ≃ᵃL[k] P₁

              Inverse of a continuous affine equivalence as a continuous affine equivalence.

              Equations
              • e.symm = { toAffineEquiv := (e).symm, continuous_toFun := , continuous_invFun := }
              Instances For
                @[simp]
                theorem ContinuousAffineEquiv.symm_toAffineEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                (e).symm = e.symm
                @[simp]
                theorem ContinuousAffineEquiv.symm_toEquiv {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                (e).symm = (e.symm).toEquiv
                @[simp]
                theorem ContinuousAffineEquiv.apply_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (p : P₂) :
                e (e.symm p) = p
                @[simp]
                theorem ContinuousAffineEquiv.symm_apply_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (p : P₁) :
                e.symm (e p) = p
                theorem ContinuousAffineEquiv.apply_eq_iff_eq_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) {p₁ : P₁} {p₂ : P₂} :
                e p₁ = p₂ p₁ = e.symm p₂
                theorem ContinuousAffineEquiv.apply_eq_iff_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) {p₁ : P₁} {p₂ : P₁} :
                e p₁ = e p₂ p₁ = p₂
                @[simp]
                theorem ContinuousAffineEquiv.symm_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                e.symm.symm = e
                theorem ContinuousAffineEquiv.symm_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (x : P₁) :
                e.symm.symm x = e x
                theorem ContinuousAffineEquiv.symm_apply_eq {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) {x : P₂} {y : P₁} :
                e.symm x = y x = e y
                theorem ContinuousAffineEquiv.eq_symm_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) {x : P₂} {y : P₁} :
                y = e.symm x e y = x
                @[simp]
                theorem ContinuousAffineEquiv.image_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (f : P₁ ≃ᵃL[k] P₂) (s : Set P₂) :
                f.symm '' s = f ⁻¹' s
                @[simp]
                theorem ContinuousAffineEquiv.preimage_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (f : P₁ ≃ᵃL[k] P₂) (s : Set P₁) :
                f.symm ⁻¹' s = f '' s
                theorem ContinuousAffineEquiv.bijective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                theorem ContinuousAffineEquiv.surjective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                theorem ContinuousAffineEquiv.injective {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                theorem ContinuousAffineEquiv.image_eq_preimage {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₁) :
                e '' s = e.symm ⁻¹' s
                theorem ContinuousAffineEquiv.image_symm_eq_preimage {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₂) :
                e.symm '' s = e ⁻¹' s
                @[simp]
                theorem ContinuousAffineEquiv.image_preimage {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₂) :
                e '' (e ⁻¹' s) = s
                @[simp]
                theorem ContinuousAffineEquiv.preimage_image {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₁) :
                e ⁻¹' (e '' s) = s
                theorem ContinuousAffineEquiv.symm_image_image {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₁) :
                e.symm '' (e '' s) = s
                theorem ContinuousAffineEquiv.image_symm_image {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) (s : Set P₂) :
                e '' (e.symm '' s) = s
                @[simp]
                theorem ContinuousAffineEquiv.refl_symm {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] :
                @[simp]
                theorem ContinuousAffineEquiv.symm_refl {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] :
                def ContinuousAffineEquiv.trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₁] [TopologicalSpace P₂] [TopologicalSpace P₃] (e : P₁ ≃ᵃL[k] P₂) (e' : P₂ ≃ᵃL[k] P₃) :
                P₁ ≃ᵃL[k] P₃

                Composition of two ContinuousAffineEquivalences, applied left to right.

                Equations
                • e.trans e' = { toAffineEquiv := (e).trans e', continuous_toFun := , continuous_invFun := }
                Instances For
                  @[simp]
                  theorem ContinuousAffineEquiv.coe_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₁] [TopologicalSpace P₂] [TopologicalSpace P₃] (e : P₁ ≃ᵃL[k] P₂) (e' : P₂ ≃ᵃL[k] P₃) :
                  (e.trans e') = e' e
                  @[simp]
                  theorem ContinuousAffineEquiv.trans_apply {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₁] [TopologicalSpace P₂] [TopologicalSpace P₃] (e : P₁ ≃ᵃL[k] P₂) (e' : P₂ ≃ᵃL[k] P₃) (p : P₁) :
                  (e.trans e') p = e' (e p)
                  theorem ContinuousAffineEquiv.trans_assoc {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8} {V₄ : Type u_9} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₁] [TopologicalSpace P₂] [TopologicalSpace P₃] [TopologicalSpace P₄] (e₁ : P₁ ≃ᵃL[k] P₂) (e₂ : P₂ ≃ᵃL[k] P₃) (e₃ : P₃ ≃ᵃL[k] P₄) :
                  (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃)
                  @[simp]
                  theorem ContinuousAffineEquiv.trans_refl {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                  e.trans (ContinuousAffineEquiv.refl k P₂) = e
                  @[simp]
                  theorem ContinuousAffineEquiv.refl_trans {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                  (ContinuousAffineEquiv.refl k P₁).trans e = e
                  @[simp]
                  theorem ContinuousAffineEquiv.self_trans_symm {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                  e.trans e.symm = ContinuousAffineEquiv.refl k P₁
                  @[simp]
                  theorem ContinuousAffineEquiv.symm_trans_self {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₁] [TopologicalSpace P₂] (e : P₁ ≃ᵃL[k] P₂) :
                  e.symm.trans e = ContinuousAffineEquiv.refl k P₂
                  def ContinuousLinearEquiv.toContinuousAffineEquiv {k : Type u_1} [Ring k] {E : Type u_10} {F : Type u_11} [AddCommGroup E] [Module k E] [TopologicalSpace E] [AddCommGroup F] [Module k F] [TopologicalSpace F] (L : E ≃L[k] F) :

                  Reinterpret a continuous linear equivalence between modules as a continuous affine equivalence.

                  Equations
                  • L.toContinuousAffineEquiv = { toAffineEquiv := L.toAffineEquiv, continuous_toFun := , continuous_invFun := }
                  Instances For
                    @[simp]
                    theorem ContinuousLinearEquiv.coe_toContinuousAffineEquiv {k : Type u_1} [Ring k] {E : Type u_10} {F : Type u_11} [AddCommGroup E] [Module k E] [TopologicalSpace E] [AddCommGroup F] [Module k F] [TopologicalSpace F] (e : E ≃L[k] F) :
                    e.toContinuousAffineEquiv = e
                    def ContinuousAffineEquiv.constVAdd (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [ContinuousConstVAdd V₁ P₁] (v : V₁) :
                    P₁ ≃ᵃL[k] P₁

                    The map p ↦ v +ᵥ p as a continuous affine automorphism of an affine space on which addition is continuous.

                    Equations
                    Instances For
                      theorem ContinuousAffineEquiv.constVAdd_coe {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [ContinuousConstVAdd V₁ P₁] (v : V₁) :