Topology on the space of continuous affine maps

This file defines a topology on the space of continuous affine maps between topological affine spaces. This is the coarsest topology satisfying the following two properties:

• For every point p, the evaluation map fun f ↦ f p is continuous.
• The map fun f ↦ f.contLinear is continuous.

@[instance_reducible]

instance ContinuousAffineMap.instTopologicalSpace {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] : TopologicalSpace (P →ᴬ[R] Q)

Equations

• ContinuousAffineMap.instTopologicalSpace = TopologicalSpace.induced (fun (f : P →ᴬ[R] Q) => (⇑f, f.contLinear)) inferInstance

theorem ContinuousAffineMap.continuous_contLinear {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddGroup W] : Continuous contLinear

instance ContinuousAffineMap.instContinuousEvalConst {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] : ContinuousEvalConst (P →ᴬ[R] Q) P Q

theorem ContinuousAffineMap.continuous_rng {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] {α : Type u_8} [TopologicalSpace α] [IsTopologicalAddGroup W] {f : α → P →ᴬ[R] Q} (h₁ : ∀ (p : P), Continuous fun (x : α) => (f x) p) (h₂ : Continuous fun (x : α) => (f x).contLinear) : Continuous f

theorem ContinuousAffineMap.continuous_rng_iff {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] {α : Type u_8} [TopologicalSpace α] [IsTopologicalAddGroup W] (f : α → P →ᴬ[R] Q) : Continuous f ↔ (∀ (p : P), Continuous fun (x : α) => (f x) p) ∧ Continuous fun (x : α) => (f x).contLinear

theorem ContinuousAffineMap.continuous_rng_of_exists {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] {α : Type u_8} [TopologicalSpace α] [IsTopologicalAddGroup W] [ContinuousSMul R V] {f : α → P →ᴬ[R] Q} (h₁ : ∃ (p : P), Continuous fun (x : α) => (f x) p) (h₂ : Continuous fun (x : α) => (f x).contLinear) : Continuous f

theorem ContinuousAffineMap.continuous_const {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] : Continuous (const R P)

instance ContinuousAffineMap.instIsTopologicalAddTorsor {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddGroup W] : IsTopologicalAddTorsor (P →ᴬ[R] Q)

instance ContinuousAffineMap.instT0Space {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [T0Space W] : T0Space (P →ᴬ[R] Q)

instance ContinuousAffineMap.instRegularSpace {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] : RegularSpace (P →ᴬ[R] Q)

theorem ContinuousAffineMap.continuous_precomp {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} {Q : Type u_6} {Q₂ : Type u_7} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [AddTorsor W₂ Q₂] [TopologicalSpace Q₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddTorsor Q₂] (g : P →ᴬ[R] Q) [ContinuousConstSMul R W₂] : Continuous fun (f : Q →ᴬ[R] Q₂) => f.comp g

def ContinuousAffineMap.precompL {R : Type u_1} {V : Type u_2} {W : Type u_3} (W₂ : Type u_4) {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (g : P →ᴬ[R] Q) : (Q →ᴬ[R] W₂) →L[R] P →ᴬ[R] W₂

Pre-composition by a fixed continuous affine map, as a continuous linear map.

Equations

• ContinuousAffineMap.precompL W₂ g = { toFun := fun (f : Q →ᴬ[R] W₂) => f.comp g, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousAffineMap.precompL_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} (W₂ : Type u_4) {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (g : P →ᴬ[R] Q) (f : Q →ᴬ[R] W₂) : (precompL W₂ g) f = f.comp g

def ContinuousAffineMap.precompA {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} {Q : Type u_6} (Q₂ : Type u_7) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [AddTorsor W₂ Q₂] [TopologicalSpace Q₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddTorsor Q₂] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (g : P →ᴬ[R] Q) : (Q →ᴬ[R] Q₂) →ᴬ[R] P →ᴬ[R] Q₂

Pre-composition by a fixed continuous affine map, as a continuous affine map.

Equations

• ContinuousAffineMap.precompA Q₂ g = { toFun := fun (f : Q →ᴬ[R] Q₂) => f.comp g, linear := ↑(ContinuousAffineMap.precompL W₂ g), map_vadd' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousAffineMap.precompA_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} {Q : Type u_6} {Q₂ : Type u_7} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [AddTorsor W₂ Q₂] [TopologicalSpace Q₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddTorsor Q₂] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (g : P →ᴬ[R] Q) (f : Q →ᴬ[R] Q₂) : (precompA Q₂ g) f = f.comp g

@[simp]

theorem ContinuousAffineMap.precompA_contLinear {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} {Q : Type u_6} {Q₂ : Type u_7} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [AddTorsor W₂ Q₂] [TopologicalSpace Q₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddTorsor Q₂] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (g : P →ᴬ[R] Q) : (precompA Q₂ g).contLinear = precompL W₂ g

@[simp]

theorem ContinuousAffineMap.precompL_toContinuousAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} {Q : Type u_6} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (g : P →ᴬ[R] Q) : (precompL W₂ g).toContinuousAffineMap = precompA W₂ g

theorem ContinuousAffineMap.continuous_postcomp {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} {Q : Type u_6} {Q₂ : Type u_7} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [AddTorsor W₂ Q₂] [TopologicalSpace Q₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddTorsor Q₂] (f : Q →ᴬ[R] Q₂) [ContinuousConstSMul R W] [ContinuousConstSMul R W₂] : Continuous fun (g : P →ᴬ[R] Q) => f.comp g

def ContinuousLinearMap.postcompContinuousAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} (P : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (f : W →L[R] W₂) : (P →ᴬ[R] W) →L[R] P →ᴬ[R] W₂

Post-composition of continuous affine maps by a fixed continuous linear map, as a continuous linear map.

Equations

• ContinuousLinearMap.postcompContinuousAffineMap P f = { toFun := fun (g : P →ᴬ[R] W) => f.toContinuousAffineMap.comp g, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.postcompContinuousAffineMap_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} (P : Type u_5) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (f : W →L[R] W₂) (g : P →ᴬ[R] W) : (postcompContinuousAffineMap P f) g = f.toContinuousAffineMap.comp g

def ContinuousAffineMap.postcompA {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} (P : Type u_5) {Q : Type u_6} {Q₂ : Type u_7} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [AddTorsor W₂ Q₂] [TopologicalSpace Q₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddTorsor Q₂] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (f : Q →ᴬ[R] Q₂) : (P →ᴬ[R] Q) →ᴬ[R] P →ᴬ[R] Q₂

Post-composition by a fixed continuous affine map, as a continuous affine map.

Equations

• ContinuousAffineMap.postcompA P f = { toFun := fun (g : P →ᴬ[R] Q) => f.comp g, linear := ↑(ContinuousLinearMap.postcompContinuousAffineMap P f.contLinear), map_vadd' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousAffineMap.postcompA_apply {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} {Q : Type u_6} {Q₂ : Type u_7} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [AddTorsor W₂ Q₂] [TopologicalSpace Q₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddTorsor Q₂] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (f : Q →ᴬ[R] Q₂) (g : P →ᴬ[R] Q) : (postcompA P f) g = f.comp g

@[simp]

theorem ContinuousAffineMap.postcompA_contLinear {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} {Q : Type u_6} {Q₂ : Type u_7} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [AddTorsor W₂ Q₂] [TopologicalSpace Q₂] [IsTopologicalAddTorsor P] [IsTopologicalAddTorsor Q] [IsTopologicalAddTorsor Q₂] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (f : Q →ᴬ[R] Q₂) : (postcompA P f).contLinear = ContinuousLinearMap.postcompContinuousAffineMap P f.contLinear

@[simp]

theorem ContinuousLinearMap.postcompContinuousAffineMap_toContinuousAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} {W₂ : Type u_4} {P : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddCommGroup W₂] [Module R W₂] [TopologicalSpace W₂] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddGroup W₂] [ContinuousConstSMul R W₂] (g : W →L[R] W₂) : (postcompContinuousAffineMap P g).toContinuousAffineMap = ContinuousAffineMap.postcompA P g.toContinuousAffineMap

instance ContinuousAffineMap.instIsTopologicalAddGroup {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] : IsTopologicalAddGroup (P →ᴬ[R] W)

instance ContinuousAffineMap.instContinuousConstSMul {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] {S : Type u_8} [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] : ContinuousConstSMul S (P →ᴬ[R] W)

instance ContinuousAffineMap.instContinuousSMul {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_5} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddTorsor P] [IsTopologicalAddGroup W] [ContinuousSMul R W] : ContinuousSMul R (P →ᴬ[R] W)

theorem ContinuousLinearMap.continuous_toContinuousAffineMap {R : Type u_1} {V : Type u_2} {W : Type u_3} [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] : Continuous toContinuousAffineMap

def ContinuousAffineMap.decompHomeomorph (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [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 homeomorphic to the product of the codomain with the space of continuous linear maps, by taking the value of the affine map at (0 : V) and the linear part.

Equations

• ContinuousAffineMap.decompHomeomorph R V Q = { toEquiv := ContinuousAffineMap.decompEquiv R V Q, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousAffineMap.fst_decompHomeomorph (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompHomeomorph R V Q) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompHomeomorph (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompHomeomorph R V Q) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompHomeomorph_symm_apply (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) (x : V) : ((decompHomeomorph R V Q).symm p) x = p.2 x +ᵥ p.1

@[simp]

theorem ContinuousAffineMap.decompHomeomorph_symm_contLinear (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) : ((decompHomeomorph R V Q).symm p).contLinear = p.2

def ContinuousAffineMap.decompContinuousLinearEquiv (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] : (V →ᴬ[R] W) ≃L[R] W × (V →L[R] W)

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

Equations

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

@[simp]

theorem ContinuousAffineMap.fst_decompContinuousLinearEquiv (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] (f : V →ᴬ[R] W) : ((decompContinuousLinearEquiv R V W) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompContinuousLinearEquiv (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] (f : V →ᴬ[R] W) : ((decompContinuousLinearEquiv R V W) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompContinuousLinearEquiv_symm_apply (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] (p : W × (V →L[R] W)) (x : V) : ((decompContinuousLinearEquiv R V W).symm p) x = p.2 x +ᵥ p.1

@[simp]

theorem ContinuousAffineMap.decompContinuousLinearEquiv_symm_contLinear (R : Type u_1) (V : Type u_2) (W : Type u_3) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] (p : W × (V →L[R] W)) : ((decompContinuousLinearEquiv R V W).symm p).contLinear = p.2

def ContinuousAffineMap.decompContinuousAffineEquiv (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] : (V →ᴬ[R] Q) ≃ᴬ[R] Q × (V →L[R] W)

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

Equations

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

@[simp]

theorem ContinuousAffineMap.fst_decompContinuousAffineEquiv (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompContinuousAffineEquiv R V Q) f).1 = f 0

@[simp]

theorem ContinuousAffineMap.snd_decompContinuousAffineEquiv (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] (f : V →ᴬ[R] Q) : ((decompContinuousAffineEquiv R V Q) f).2 = f.contLinear

@[simp]

theorem ContinuousAffineMap.decompContinuousAffineEquiv_symm_apply (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) (x : V) : ((decompContinuousAffineEquiv R V Q).symm p) x = p.2 x +ᵥ p.1

@[simp]

theorem ContinuousAffineMap.decompContinuousAffineEquiv_symm_contLinear (R : Type u_1) (V : Type u_2) {W : Type u_3} (Q : Type u_6) [NormedField R] [AddCommGroup V] [Module R V] [TopologicalSpace V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddGroup V] [ContinuousSMul R V] [IsTopologicalAddGroup W] [ContinuousConstSMul R W] [IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) : ((decompContinuousAffineEquiv R V Q).symm p).contLinear = p.2