Continuous affine maps.

This file defines a type of bundled continuous affine maps.

Main definitions:

• ContinuousAffineMap

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

• 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

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.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

• ContinuousAffineMap.instFunLike = { coe := fun (f : P →ᴬ[R] Q) => ⇑↑f, 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

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 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

• 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_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) : 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 as a continuous affine map

Equations

• ContinuousAffineMap.const R P q = { toAffineMap := AffineMap.const R P q, 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) : ⇑(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.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] : P →ᴬ[R] P

The identity map as a continuous affine map

Equations

• ContinuousAffineMap.id R P = { toAffineMap := AffineMap.id R P, cont := ⋯ }

@[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 := ⋯ }

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

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

Equations

• ContinuousAffineMap.lineMap p₀ p₁ = { toAffineMap := AffineMap.lineMap p₀ p₁, cont := ⋯ }

@[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₁)

def ContinuousAffineMap.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) : V →L[R] W

The linear map underlying a continuous affine map is continuous.

Equations

• f.contLinear = { toFun := ⇑(↑f).linear, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[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_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) : ↑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.

theorem ContinuousAffineMap.coe_linear_eq_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).linear = ⇑f.contLinear

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

@[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]

theorem ContinuousAffineMap.const_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] (q : Q) : (const R P q).contLinear = 0

theorem ContinuousAffineMap.contLinear_eq_zero_iff_exists_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] [TopologicalSpace V] [IsTopologicalAddTorsor P] [TopologicalSpace W] [IsTopologicalAddTorsor Q] (f : P →ᴬ[R] Q) : f.contLinear = 0 ↔ ∃ (q : Q), f = const R P q

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_10} [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 := __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_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

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_10} [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)

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_10} [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 ⋯ ⋯

@[simp]

theorem ContinuousAffineMap.smul_contLinear {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] [TopologicalSpace V] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] (t : S) (f : P →ᴬ[R] W) : (t • f).contLinear = t • f.contLinear

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

• ContinuousAffineMap.instAdd = { add := fun (f g : P →ᴬ[R] W) => let __src := ↑f + ↑g; { 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] [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

• ContinuousAffineMap.instSub = { sub := fun (f g : P →ᴬ[R] W) => let __src := ↑f - ↑g; { 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] [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

• ContinuousAffineMap.instNeg = { neg := fun (f : P →ᴬ[R] W) => let __src := -↑f; { 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] [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

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] [IsTopologicalAddGroup 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_10} [TopologicalSpace W] [IsTopologicalAddGroup 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_10} [TopologicalSpace W] [IsTopologicalAddGroup 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' := ⋯ } ⋯ ⋯

@[simp]

theorem ContinuousAffineMap.zero_contLinear {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] [TopologicalSpace V] [IsTopologicalAddTorsor P] : contLinear 0 = 0

@[simp]

theorem ContinuousAffineMap.add_contLinear {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] [TopologicalSpace V] [IsTopologicalAddTorsor P] (f g : P →ᴬ[R] W) : (f + g).contLinear = f.contLinear + g.contLinear

@[simp]

theorem ContinuousAffineMap.sub_contLinear {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] [TopologicalSpace V] [IsTopologicalAddTorsor P] (f g : P →ᴬ[R] W) : (f - g).contLinear = f.contLinear - g.contLinear

@[simp]

theorem ContinuousAffineMap.neg_contLinear {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] [TopologicalSpace V] [IsTopologicalAddTorsor P] (f : P →ᴬ[R] W) : (-f).contLinear = -f.contLinear

instance ContinuousAffineMap.instAddTorsor {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] : AddTorsor (P →ᴬ[R] W) (P →ᴬ[R] Q)

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

@[simp]

theorem ContinuousAffineMap.vadd_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 W] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] [TopologicalSpace V] [IsTopologicalAddTorsor P] (f : P →ᴬ[R] W) (g : P →ᴬ[R] Q) : (f +ᵥ g).contLinear = f.contLinear + g.contLinear

@[simp]

theorem ContinuousAffineMap.vsub_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 W] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] [TopologicalSpace V] [IsTopologicalAddTorsor P] (f g : P →ᴬ[R] Q) : (f -ᵥ g).contLinear = f.contLinear - g.contLinear

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 := ⋯ }

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

• f.prodMap g = { toAffineMap := (↑f).prodMap ↑g, cont := ⋯ }

@[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₃) : (f.prod g).contLinear = f.contLinear.prod g.contLinear

@[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₄) : (f.prodMap g).contLinear = f.contLinear.prodMap g.contLinear

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

@[simp]

theorem ContinuousLinearMap.toContinuousAffineMap_contLinear {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] [IsTopologicalAddGroup V] [IsTopologicalAddGroup W] (f : V →L[R] W) : f.toContinuousAffineMap.contLinear = f

@[deprecated ContinuousLinearMap.toContinuousAffineMap_contLinear (since := "2025-09-23")]

theorem ContinuousAffineMap.to_affine_map_contLinear {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] [IsTopologicalAddGroup V] [IsTopologicalAddGroup W] (f : V →L[R] W) : f.toContinuousAffineMap.contLinear = f

Alias of ContinuousLinearMap.toContinuousAffineMap_contLinear.

theorem ContinuousAffineMap.decomp {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] [IsTopologicalAddGroup V] [IsTopologicalAddGroup W] (f : V →ᴬ[R] W) : ⇑f = ⇑f.contLinear + Function.const V (f 0)