Continuous affine maps.

This file defines a type of bundled continuous affine maps.

Note that the definition and basic properties established here require minimal assumptions, and do not even assume compatibility between the topological and algebraic structures. Of course it is necessary to assume some compatibility in order to obtain a useful theory. Such a theory is developed elsewhere for affine spaces modelled on normed vector spaces, but not yet for general topological affine spaces (since we have not defined these yet).

Main definitions:

• ContinuousAffineMap

Notation:

We introduce the notation P →ᴬ[R] Q for ContinuousAffineMap R P Q. 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 AffineMap : Type (max (max (max u_2 u_3) u_4) u_5)

A continuous map of affine spaces.

• toFun : P → Q
• linear : V →ₗ[R] W
• map_vadd' : ∀ (p : P) (v : V), self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun p
• cont : Continuous self.toFun

theorem ContinuousAffineMap.cont {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] (self : P →ᴬ[R] Q) : Continuous self.toFun

def «term_→ᴬ[_]_» : Lean.TrailingParserDescr

A continuous map of affine spaces.

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousAffineMap.instCoeAffineMap {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] : Coe (P →ᴬ[R] Q) (P →ᵃ[R] Q)

Equations

• ContinuousAffineMap.instCoeAffineMap = { coe := ContinuousAffineMap.toAffineMap }

theorem ContinuousAffineMap.to_affineMap_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 : P →ᴬ[R] Q} {g : P →ᴬ[R] Q} (h : f.toAffineMap = g.toAffineMap) : 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

• ContinuousAffineMap.instFunLike = { coe := fun (f : P →ᴬ[R] Q) => ⇑f.toAffineMap, coe_injective' := ⋯ }

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] : ContinuousMapClass (P →ᴬ[R] Q) P Q

Equations

• ⋯ = ⋯

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.coe_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] : Function.Injective DFunLike.coe

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 : P →ᴬ[R] Q} {g : P →ᴬ[R] Q} (h : ∀ (x : P), f x = g x) : f = g

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 : P →ᴬ[R] Q} {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

• f.toContinuousMap = { toFun := ⇑f, continuous_toFun := ⋯ }

instance ContinuousAffineMap.instCoeHeadContinuousMap {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] : CoeHead (P →ᴬ[R] Q) C(P, Q)

Equations

• ContinuousAffineMap.instCoeHeadContinuousMap = { coe := ContinuousAffineMap.toContinuousMap }

@[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) : f.toContinuousMap = ↑f

@[simp]

theorem ContinuousAffineMap.coe_to_affineMap {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.toAffineMap = ⇑f

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 : P →ᴬ[R] Q} {g : P →ᴬ[R] Q} (h : ↑f = ↑g) : f = g

theorem ContinuousAffineMap.coe_affineMap_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 }.toAffineMap = 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.toAffineMap, 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) : Continuous ⇑f

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) : P →ᴬ[R] Q

The constant map is a continuous affine map.

Equations

• ContinuousAffineMap.const R P q = { toFun := ⇑(AffineMap.const R P q), linear := (AffineMap.const R P q).linear, map_vadd' := ⋯, cont := ⋯ }

@[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) : ⇑(ContinuousAffineMap.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] : Inhabited (P →ᴬ[R] Q)

Equations

• ContinuousAffineMap.instInhabited R P = { default := ContinuousAffineMap.const R P ⋯.some }

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 morphisms is a morphism.

Equations

• f.comp g = { toAffineMap := f.comp g.toAffineMap, cont := ⋯ }

@[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) (x : P) : (f.comp g) x = f (g x)

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

• ContinuousAffineMap.instZero = { zero := ContinuousAffineMap.const R P 0 }

@[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_8} [TopologicalSpace W] [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] : SMul S (P →ᴬ[R] W)

Equations

• ContinuousAffineMap.instSMul = { smul := fun (t : S) (f : P →ᴬ[R] W) => let __src := t • f.toAffineMap; { toAffineMap := __src, cont := ⋯ } }

@[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_8} [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_8} [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

instance ContinuousAffineMap.instIsCentralScalar {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_8} [TopologicalSpace W] [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [DistribMulAction Sᵐᵒᵖ W] [IsCentralScalar S W] : IsCentralScalar S (P →ᴬ[R] W)

Equations

• ⋯ = ⋯

instance ContinuousAffineMap.instMulAction {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_8} [TopologicalSpace W] [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] : MulAction S (P →ᴬ[R] W)

Equations

• ContinuousAffineMap.instMulAction = Function.Injective.mulAction DFunLike.coe ⋯ ⋯

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] [TopologicalAddGroup W] : Add (P →ᴬ[R] W)

Equations

• ContinuousAffineMap.instAdd = { add := fun (f g : P →ᴬ[R] W) => let __src := f.toAffineMap + g.toAffineMap; { toAffineMap := __src, cont := ⋯ } }

@[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] [TopologicalAddGroup W] (f : P →ᴬ[R] W) (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] [TopologicalAddGroup W] (f : P →ᴬ[R] W) (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] [TopologicalAddGroup W] : Sub (P →ᴬ[R] W)

Equations

• ContinuousAffineMap.instSub = { sub := fun (f g : P →ᴬ[R] W) => let __src := f.toAffineMap - g.toAffineMap; { toAffineMap := __src, cont := ⋯ } }

@[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] [TopologicalAddGroup W] (f : P →ᴬ[R] W) (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] [TopologicalAddGroup W] (f : P →ᴬ[R] W) (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] [TopologicalAddGroup W] : Neg (P →ᴬ[R] W)

Equations

• ContinuousAffineMap.instNeg = { neg := fun (f : P →ᴬ[R] W) => let __src := -f.toAffineMap; { toAffineMap := __src, cont := ⋯ } }

@[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] [TopologicalAddGroup 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] [TopologicalAddGroup W] (f : P →ᴬ[R] W) (x : P) : (-f) x = -f x

instance ContinuousAffineMap.instAddCommGroup {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] [TopologicalAddGroup W] : AddCommGroup (P →ᴬ[R] W)

Equations

• ContinuousAffineMap.instAddCommGroup = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance ContinuousAffineMap.instDistribMulActionOfSMulCommClassOfContinuousConstSMul {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_8} [TopologicalSpace W] [TopologicalAddGroup W] [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] : DistribMulAction S (P →ᴬ[R] W)

Equations

• ContinuousAffineMap.instDistribMulActionOfSMulCommClassOfContinuousConstSMul = Function.Injective.distribMulAction { toFun := fun (f : P →ᴬ[R] W) => f.toFun, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul {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_8} [TopologicalSpace W] [TopologicalAddGroup W] [Semiring S] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] : Module S (P →ᴬ[R] W)

Equations

• ContinuousAffineMap.instModuleOfSMulCommClassOfContinuousConstSMul = Function.Injective.module S { toFun := fun (f : P →ᴬ[R] W) => f.toFun, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

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) : V →ᴬ[R] W

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

Equations

• f.toContinuousAffineMap = { toFun := ⇑f, linear := ↑f, map_vadd' := ⋯, cont := ⋯ }

@[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) : ⇑f.toContinuousAffineMap = ⇑f

@[simp]

theorem ContinuousLinearMap.toContinuousAffineMap_map_zero {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) : f.toContinuousAffineMap 0 = 0