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

@[implicit_reducible]

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)

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

@[implicit_reducible]

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

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.

@[implicit_reducible]

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)

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

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

@[implicit_reducible]

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)

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

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

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

@[simp]

theorem ContinuousAffineMap.apply_lineMap {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) (p₀ p₁ : P) (c : R) : f ((AffineMap.lineMap p₀ p₁) c) = (AffineMap.lineMap (f p₀) (f p₁)) c

Applying a ContinuousAffineMap commutes with AffineMap.lineMap.

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₁

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

@[simp]

theorem ContinuousAffineMap.apply_lineMap' {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 R] [TopologicalSpace V] [TopologicalSpace W] [ContinuousSMul R V] [ContinuousSMul R W] [ContinuousVAdd V P] [ContinuousVAdd W Q] (f : P →ᴬ[R] Q) (p₀ p₁ : P) (c : R) : f ((lineMap p₀ p₁) c) = (lineMap (f p₀) (f p₁)) c

Applying a ContinuousAffineMap commutes with ContinuousAffineMap.lineMap.

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.

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

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

@[implicit_reducible]

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)

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

@[implicit_reducible]

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)

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

@[implicit_reducible]

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)

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

@[implicit_reducible]

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)

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

@[implicit_reducible]

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)

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

@[implicit_reducible]

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)

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

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

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

@[implicit_reducible]

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.

@[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.lineMap_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] [ContinuousConstSMul R W] [SMulCommClass R R W] (f g : P →ᴬ[R] Q) (c : R) (p : P) : ((AffineMap.lineMap f g) c) p = (AffineMap.lineMap (f p) (g p)) c

Interpolating between ContinuousAffineMaps with AffineMap.lineMap commutes with evaluation.

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

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

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

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

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)

def ContinuousAffineMap.decompEquiv (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] : (V →ᴬ[R] Q) ≃ Q × (V →L[R] W)

The space of continuous affine maps from a topological vector space to a topological affine space is in bijection with the product of the codomain with the space of linear maps, by taking the value of the affine map at (0 : V) and the linear part.

@[simp]

theorem ContinuousAffineMap.fst_decompEquiv (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompEquiv R V Q) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompEquiv (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompEquiv R V Q) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompEquiv_symm_apply (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) (x : V) : ((decompEquiv R V Q).symm p) x = p.2 x +ᵥ p.1

@[simp]

theorem ContinuousAffineMap.decompEquiv_symm_contLinear (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) : ((decompEquiv R V Q).symm p).contLinear = p.2

def ContinuousAffineMap.decompLinearEquiv (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [IsTopologicalAddGroup W] : (V →ᴬ[R] W) ≃ₗ[S] W × (V →L[R] W)

The space of continuous affine maps between topological vector spaces is linearly isomorphic to the product of the codomain with the space of linear maps, by taking the value of the affine map at (0 : V) and the linear part.

@[simp]

theorem ContinuousAffineMap.fst_decompLinearEquiv (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [IsTopologicalAddGroup W] (f : V →ᴬ[R] W) : ((decompLinearEquiv R S V W) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompLinearEquiv (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [IsTopologicalAddGroup W] (f : V →ᴬ[R] W) : ((decompLinearEquiv R S V W) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompLinearEquiv_symm_apply (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [IsTopologicalAddGroup W] (p : W × (V →L[R] W)) (x : V) : ((decompLinearEquiv R S V W).symm p) x = p.2 x + p.1

@[simp]

theorem ContinuousAffineMap.decompLinearEquiv_symm_contLinear (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [IsTopologicalAddGroup W] (p : W × (V →L[R] W)) : ((decompLinearEquiv R S V W).symm p).contLinear = p.2

def ContinuousAffineMap.decompAffineEquiv (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] : (V →ᴬ[R] Q) ≃ᵃ[S] Q × (V →L[R] W)

The space of continuous affine maps from a topological vector space to a topological affine space is affinely isomorphic to the product of the codomain with the space of linear maps, by taking the value of the affine map at (0 : V) and the linear part.

@[simp]

theorem ContinuousAffineMap.linear_decompAffineEquiv (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] : (decompAffineEquiv R S V Q).linear = decompLinearEquiv R S V W

@[simp]

theorem ContinuousAffineMap.fst_decompAffineEquiv (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompAffineEquiv R S V Q) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompAffineEquiv (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompAffineEquiv R S V Q) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompAffineEquiv_symm_apply (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) (x : V) : ((decompAffineEquiv R S V Q).symm p) x = p.2 x +ᵥ p.1

@[simp]

theorem ContinuousAffineMap.decompAffineEquiv_symm_contLinear (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [Ring S] [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) : ((decompAffineEquiv R S V Q).symm p).contLinear = p.2