Documentation

Mathlib.Topology.Algebra.ContinuousAffineMap

Continuous affine maps. #

This file defines a type of bundled continuous affine maps.

Main definitions: #

Notation: #

We introduce the notation P →ᴬ[R] Q for ContinuousAffineMap R P Q (not to be confused with the notation A →A[R] B for ContinuousAlgHom). Note that this is parallel to the notation E →L[R] F for ContinuousLinearMap R E F.

structure ContinuousAffineMap (R : Type u_1) {V : Type u_2} {W : Type u_3} (P : Type u_4) (Q : Type u_5) [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] extends P →ᵃ[R] Q :
Type (max (max (max u_2 u_3) u_4) u_5)

A continuous map of affine spaces

Instances For

    A continuous map of affine spaces

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem ContinuousAffineMap.toAffineMap_injective {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {f g : P →ᴬ[R] Q} (h : f = g) :
      f = g
      instance ContinuousAffineMap.instFunLike {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] :
      FunLike (P →ᴬ[R] Q) P Q
      Equations
      instance ContinuousAffineMap.instContinuousMapClass {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] :
      theorem ContinuousAffineMap.toFun_eq_coe {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) :
      (↑f).toFun = f
      theorem ContinuousAffineMap.ext {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {f g : P →ᴬ[R] Q} (h : ∀ (x : P), f x = g x) :
      f = g
      theorem ContinuousAffineMap.ext_iff {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {f g : P →ᴬ[R] Q} :
      f = g ∀ (x : P), f x = g x
      theorem ContinuousAffineMap.congr_fun {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {f g : P →ᴬ[R] Q} (h : f = g) (x : P) :
      f x = g x
      def ContinuousAffineMap.toContinuousMap {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) :
      C(P, Q)

      Forgetting its algebraic properties, a continuous affine map is a continuous map.

      Equations
      Instances For
        @[simp]
        theorem ContinuousAffineMap.toContinuousMap_coe {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) :
        @[simp]
        theorem ContinuousAffineMap.coe_toAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) :
        f = f
        @[simp]
        theorem ContinuousAffineMap.coe_to_continuousMap {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) :
        f = f
        theorem ContinuousAffineMap.to_continuousMap_injective {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {f g : P →ᴬ[R] Q} (h : f = g) :
        f = g
        theorem ContinuousAffineMap.coe_toAffineMap_mk {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᵃ[R] Q) (h : Continuous f.toFun) :
        { toAffineMap := f, cont := h } = f
        theorem ContinuousAffineMap.coe_continuousMap_mk {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᵃ[R] Q) (h : Continuous f.toFun) :
        { toAffineMap := f, cont := h } = { toFun := f, continuous_toFun := h }
        @[simp]
        theorem ContinuousAffineMap.coe_mk {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᵃ[R] Q) (h : Continuous f.toFun) :
        { toAffineMap := f, cont := h } = f
        @[simp]
        theorem ContinuousAffineMap.mk_coe {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) (h : Continuous (↑f).toFun) :
        { toAffineMap := f, cont := h } = f
        theorem ContinuousAffineMap.continuous {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) :
        def ContinuousAffineMap.const (R : Type u_1) {V : Type u_2} {W : Type u_3} (P : Type u_4) {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (q : Q) :

        The constant map as a continuous affine map

        Equations
        Instances For
          @[simp]
          theorem ContinuousAffineMap.coe_const (R : Type u_1) {V : Type u_2} {W : Type u_3} (P : Type u_4) {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (q : Q) :
          (const R P q) = Function.const P q
          noncomputable instance ContinuousAffineMap.instInhabited (R : Type u_1) {V : Type u_2} {W : Type u_3} (P : Type u_4) {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] :
          Equations
          def ContinuousAffineMap.id (R : Type u_1) {V : Type u_2} (P : Type u_4) [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] :

          The identity map as a continuous affine map

          Equations
          Instances For
            @[simp]
            theorem ContinuousAffineMap.coe_id (R : Type u_1) {V : Type u_2} (P : Type u_4) [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] :
            (id R P) = _root_.id
            def ContinuousAffineMap.comp {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {W₂ : Type u_6} {Q₂ : Type u_7} [AddCommGroup W₂] [Module R W₂] [TopologicalSpace Q₂] [AddTorsor W₂ Q₂] (f : Q →ᴬ[R] Q₂) (g : P →ᴬ[R] Q) :
            P →ᴬ[R] Q₂

            The composition of continuous affine maps as a continuous affine map

            Equations
            • f.comp g = { toAffineMap := (↑f).comp g, cont := }
            Instances For
              @[simp]
              theorem ContinuousAffineMap.coe_comp {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {W₂ : Type u_6} {Q₂ : Type u_7} [AddCommGroup W₂] [Module R W₂] [TopologicalSpace Q₂] [AddTorsor W₂ Q₂] (f : Q →ᴬ[R] Q₂) (g : P →ᴬ[R] Q) :
              (f.comp g) = f g
              theorem ContinuousAffineMap.comp_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {W₂ : Type u_6} {Q₂ : Type u_7} [AddCommGroup W₂] [Module R W₂] [TopologicalSpace Q₂] [AddTorsor W₂ Q₂] (f : Q →ᴬ[R] Q₂) (g : P →ᴬ[R] Q) (p : P) :
              (f.comp g) p = f (g p)
              @[simp]
              theorem ContinuousAffineMap.comp_id {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) :
              f.comp (id R P) = f
              @[simp]
              theorem ContinuousAffineMap.id_comp {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (f : P →ᴬ[R] Q) :
              (id R Q).comp f = f
              def ContinuousAffineMap.lineMap {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (p₀ p₁ : P) [TopologicalSpace R] [TopologicalSpace V] [ContinuousSMul R V] [ContinuousVAdd V P] :

              The continuous affine map sending 0 to p₀ and 1 to p₁

              Equations
              Instances For
                @[simp]
                theorem ContinuousAffineMap.lineMap_toAffineMap {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (p₀ p₁ : P) [TopologicalSpace R] [TopologicalSpace V] [ContinuousSMul R V] [ContinuousVAdd V P] :
                (lineMap p₀ p₁) = AffineMap.lineMap p₀ p₁
                theorem ContinuousAffineMap.coe_lineMap_eq {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (p₀ p₁ : P) [TopologicalSpace R] [TopologicalSpace V] [ContinuousSMul R V] [ContinuousVAdd V P] :
                (lineMap p₀ p₁) = (AffineMap.lineMap p₀ p₁)

                The linear map underlying a continuous affine map is continuous.

                Equations
                Instances For
                  @[simp]
                  theorem ContinuousAffineMap.coe_contLinear {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace V] [IsTopologicalAddTorsor P] [TopologicalSpace W] [IsTopologicalAddTorsor Q] (f : P →ᴬ[R] Q) :
                  f.contLinear = (↑f).linear
                  @[simp]
                  theorem ContinuousAffineMap.coe_mk_contLinear_eq_linear {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace V] [IsTopologicalAddTorsor P] [TopologicalSpace W] [IsTopologicalAddTorsor Q] (f : P →ᵃ[R] Q) (h : Continuous f.toFun) :
                  { toAffineMap := f, cont := h }.contLinear = f.linear
                  @[deprecated ContinuousAffineMap.coe_mk_contLinear_eq_linear (since := "2025-09-17")]
                  theorem ContinuousAffineMap.coe_mk_const_linear_eq_linear {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace V] [IsTopologicalAddTorsor P] [TopologicalSpace W] [IsTopologicalAddTorsor Q] (f : P →ᵃ[R] Q) (h : Continuous f.toFun) :
                  { toAffineMap := f, cont := h }.contLinear = f.linear

                  Alias of ContinuousAffineMap.coe_mk_contLinear_eq_linear.

                  @[simp]
                  theorem ContinuousAffineMap.comp_contLinear {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] {W₂ : Type u_6} {Q₂ : Type u_7} [AddCommGroup W₂] [Module R W₂] [TopologicalSpace Q₂] [AddTorsor W₂ Q₂] [TopologicalSpace V] [IsTopologicalAddTorsor P] [TopologicalSpace W] [IsTopologicalAddTorsor Q] [TopologicalSpace W₂] [IsTopologicalAddTorsor Q₂] (f : P →ᴬ[R] Q) (g : Q →ᴬ[R] Q₂) :
                  @[simp]
                  theorem ContinuousAffineMap.map_vadd {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace V] [IsTopologicalAddTorsor P] [TopologicalSpace W] [IsTopologicalAddTorsor Q] (f : P →ᴬ[R] Q) (p : P) (v : V) :
                  f (v +ᵥ p) = f.contLinear v +ᵥ f p
                  @[simp]
                  theorem ContinuousAffineMap.contLinear_map_vsub {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace V] [IsTopologicalAddTorsor P] [TopologicalSpace W] [IsTopologicalAddTorsor Q] (f : P →ᴬ[R] Q) (p₁ p₂ : P) :
                  f.contLinear (p₁ -ᵥ p₂) = f p₁ -ᵥ f p₂
                  @[simp]
                  instance ContinuousAffineMap.instZero {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] :
                  Zero (P →ᴬ[R] W)
                  Equations
                  @[simp]
                  theorem ContinuousAffineMap.coe_zero {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] :
                  0 = 0
                  theorem ContinuousAffineMap.zero_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] (x : P) :
                  0 x = 0
                  instance ContinuousAffineMap.instSMul {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] {S : Type u_10} [TopologicalSpace W] [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] :
                  SMul S (P →ᴬ[R] W)
                  Equations
                  @[simp]
                  theorem ContinuousAffineMap.coe_smul {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] {S : Type u_10} [TopologicalSpace W] [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] (t : S) (f : P →ᴬ[R] W) :
                  ⇑(t f) = t f
                  theorem ContinuousAffineMap.smul_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] {S : Type u_10} [TopologicalSpace W] [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] (t : S) (f : P →ᴬ[R] W) (x : P) :
                  (t f) x = t f x
                  @[simp]
                  instance ContinuousAffineMap.instAdd {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] :
                  Add (P →ᴬ[R] W)
                  Equations
                  @[simp]
                  theorem ContinuousAffineMap.coe_add {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] (f g : P →ᴬ[R] W) :
                  ⇑(f + g) = f + g
                  theorem ContinuousAffineMap.add_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] (f g : P →ᴬ[R] W) (x : P) :
                  (f + g) x = f x + g x
                  instance ContinuousAffineMap.instSub {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] :
                  Sub (P →ᴬ[R] W)
                  Equations
                  @[simp]
                  theorem ContinuousAffineMap.coe_sub {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] (f g : P →ᴬ[R] W) :
                  ⇑(f - g) = f - g
                  theorem ContinuousAffineMap.sub_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] (f g : P →ᴬ[R] W) (x : P) :
                  (f - g) x = f x - g x
                  instance ContinuousAffineMap.instNeg {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] :
                  Neg (P →ᴬ[R] W)
                  Equations
                  @[simp]
                  theorem ContinuousAffineMap.coe_neg {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] (f : P →ᴬ[R] W) :
                  ⇑(-f) = -f
                  theorem ContinuousAffineMap.neg_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] (f : P →ᴬ[R] W) (x : P) :
                  (-f) x = -f x
                  Equations

                  The space of continuous affine maps from P to Q is an affine space over the space of continuous affine maps from P to W.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[simp]
                  theorem ContinuousAffineMap.vadd_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace W] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f : P →ᴬ[R] W) (g : P →ᴬ[R] Q) (p : P) :
                  (f +ᵥ g) p = f p +ᵥ g p
                  @[simp]
                  theorem ContinuousAffineMap.vsub_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace W] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f g : P →ᴬ[R] Q) (p : P) :
                  (f -ᵥ g) p = f p -ᵥ g p
                  @[simp]
                  theorem ContinuousAffineMap.vadd_toAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace W] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f : P →ᴬ[R] W) (g : P →ᴬ[R] Q) :
                  ↑(f +ᵥ g) = f +ᵥ g
                  @[simp]
                  theorem ContinuousAffineMap.vsub_toAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] [TopologicalSpace W] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f g : P →ᴬ[R] Q) :
                  ↑(f -ᵥ g) = f -ᵥ g
                  def ContinuousAffineMap.prod {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) :
                  P₁ →ᴬ[k] P₂ × P₃

                  The product of two continuous affine maps is a continuous affine map.

                  Equations
                  • f.prod g = { toAffineMap := (↑f).prod g, cont := }
                  Instances For
                    @[simp]
                    theorem ContinuousAffineMap.prod_toAffineMap {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) :
                    (f.prod g) = (↑f).prod g
                    theorem ContinuousAffineMap.coe_prod {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) :
                    (f.prod g) = Pi.prod f g
                    @[simp]
                    theorem ContinuousAffineMap.prod_apply {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) (p : P₁) :
                    (f.prod g) p = (f p, g p)
                    def ContinuousAffineMap.prodMap {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} {V₄ : Type u_18} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄) :
                    P₁ × P₃ →ᴬ[k] P₂ × P₄

                    Prod.map of two continuous affine maps.

                    Equations
                    Instances For
                      @[simp]
                      theorem ContinuousAffineMap.prodMap_toAffineMap {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} {V₄ : Type u_18} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄) :
                      (f.prodMap g) = (↑f).prodMap g
                      theorem ContinuousAffineMap.coe_prodMap {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} {V₄ : Type u_18} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄) :
                      (f.prodMap g) = Prod.map f g
                      @[simp]
                      theorem ContinuousAffineMap.prodMap_apply {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} {V₄ : Type u_18} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄) (x : P₁ × P₃) :
                      (f.prodMap g) x = (f x.1, g x.2)
                      @[simp]
                      theorem ContinuousAffineMap.prod_contLinear {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [TopologicalSpace V₁] [IsTopologicalAddTorsor P₁] [TopologicalSpace V₂] [IsTopologicalAddTorsor P₂] [TopologicalSpace V₃] [IsTopologicalAddTorsor P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) :
                      @[simp]
                      theorem ContinuousAffineMap.prodMap_contLinear {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17} {V₄ : Type u_18} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] [TopologicalSpace P₃] [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄] [TopologicalSpace P₄] [TopologicalSpace V₁] [IsTopologicalAddTorsor P₁] [TopologicalSpace V₂] [IsTopologicalAddTorsor P₂] [TopologicalSpace V₃] [IsTopologicalAddTorsor P₃] [TopologicalSpace V₄] [IsTopologicalAddTorsor P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄) :
                      def ContinuousLinearMap.toContinuousAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] (f : V →L[R] W) :

                      A continuous linear map can be regarded as a continuous affine map.

                      Equations
                      Instances For
                        @[simp]
                        theorem ContinuousLinearMap.coe_toContinuousAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] (f : V →L[R] W) :
                        @[deprecated ContinuousLinearMap.toContinuousAffineMap_contLinear (since := "2025-09-23")]

                        Alias of ContinuousLinearMap.toContinuousAffineMap_contLinear.