Continuous affine maps. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines a type of bundled continuous affine maps.
Note that the definition and basic properties established here require minimal assumptions, and do not even assume compatibility between the topological and algebraic structures. Of course it is necessary to assume some compatibility in order to obtain a useful theory. Such a theory is developed elsewhere for affine spaces modelled on normed vector spaces, but not yet for general topological affine spaces (since we have not defined these yet).
Main definitions: #
Notation: #
We introduce the notation P →A[R] Q for continuous_affine_map R P Q. Note that this is parallel
to the notation E →L[R] F for continuous_linear_map R E F.
structure
continuous_affine_map
(R : Type u_1)
{V : Type u_2}
{W : Type u_3}
(P : Type u_4)
(Q : Type u_5)
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q] :
Type (max u_2 u_3 u_4 u_5)
- to_affine_map : P →ᵃ[R] Q
- cont : continuous self.to_affine_map.to_fun
A continuous map of affine spaces.
Instances for continuous_affine_map
- continuous_affine_map.has_sizeof_inst
- continuous_affine_map.affine_map.has_coe
- continuous_affine_map.continuous_map_class
- continuous_affine_map.has_coe_to_fun
- continuous_affine_map.continuous_map.has_coe
- continuous_affine_map.inhabited
- continuous_affine_map.has_zero
- continuous_affine_map.has_smul
- continuous_affine_map.is_central_scalar
- continuous_affine_map.mul_action
- continuous_affine_map.has_add
- continuous_affine_map.has_sub
- continuous_affine_map.has_neg
- continuous_affine_map.add_comm_group
- continuous_affine_map.distrib_mul_action
- continuous_affine_map.module
- continuous_affine_map.has_norm
- continuous_affine_map.normed_add_comm_group
- continuous_affine_map.normed_space
@[protected, instance]
def
continuous_affine_map.affine_map.has_coe
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q] :
Equations
theorem
continuous_affine_map.to_affine_map_injective
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
{f g : P →A[R] Q}
(h : ↑f = ↑g) :
f = g
@[protected, instance]
def
continuous_affine_map.continuous_map_class
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q] :
continuous_map_class (P →A[R] Q) P Q
Equations
- continuous_affine_map.continuous_map_class = {coe := λ (f : P →A[R] Q), ⇑(f.to_affine_map), coe_injective' := _, map_continuous := _}
@[protected, instance]
def
continuous_affine_map.has_coe_to_fun
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q] :
Helper instance for when there's too many metavariables to apply
fun_like.has_coe_to_fun directly.
theorem
continuous_affine_map.to_fun_eq_coe
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →A[R] Q) :
f.to_affine_map.to_fun = ⇑f
theorem
continuous_affine_map.coe_injective
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q] :
@[ext]
theorem
continuous_affine_map.ext
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
{f g : P →A[R] Q}
(h : ∀ (x : P), ⇑f x = ⇑g x) :
f = g
theorem
continuous_affine_map.ext_iff
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
{f g : P →A[R] Q} :
theorem
continuous_affine_map.congr_fun
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
{f g : P →A[R] Q}
(h : f = g)
(x : P) :
def
continuous_affine_map.to_continuous_map
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →A[R] Q) :
Forgetting its algebraic properties, a continuous affine map is a continuous map.
Equations
- f.to_continuous_map = {to_fun := ⇑f, continuous_to_fun := _}
@[protected, instance]
def
continuous_affine_map.continuous_map.has_coe
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q] :
Equations
@[simp]
theorem
continuous_affine_map.to_affine_map_eq_coe
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →A[R] Q) :
f.to_affine_map = ↑f
@[simp]
theorem
continuous_affine_map.to_continuous_map_coe
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →A[R] Q) :
f.to_continuous_map = ↑f
@[simp, norm_cast]
theorem
continuous_affine_map.coe_to_affine_map
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →A[R] Q) :
@[simp, norm_cast]
theorem
continuous_affine_map.coe_to_continuous_map
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →A[R] Q) :
theorem
continuous_affine_map.to_continuous_map_injective
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
{f g : P →A[R] Q}
(h : ↑f = ↑g) :
f = g
@[norm_cast]
theorem
continuous_affine_map.coe_affine_map_mk
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →ᵃ[R] Q)
(h : continuous f.to_fun) :
↑{to_affine_map := f, cont := h} = f
@[norm_cast]
theorem
continuous_affine_map.coe_continuous_map_mk
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →ᵃ[R] Q)
(h : continuous f.to_fun) :
↑{to_affine_map := f, cont := h} = {to_fun := ⇑f, continuous_to_fun := h}
@[simp]
theorem
continuous_affine_map.coe_mk
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →ᵃ[R] Q)
(h : continuous f.to_fun) :
@[simp]
theorem
continuous_affine_map.mk_coe
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →A[R] Q)
(h : continuous ↑f.to_fun) :
{to_affine_map := ↑f, cont := h} = f
@[protected, continuity]
theorem
continuous_affine_map.continuous
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(f : P →A[R] Q) :
def
continuous_affine_map.const
(R : Type u_1)
{V : Type u_2}
{W : Type u_3}
(P : Type u_4)
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(q : Q) :
The constant map is a continuous affine map.
Equations
- continuous_affine_map.const R P q = {to_affine_map := {to_fun := ⇑(affine_map.const R P q), linear := (affine_map.const R P q).linear, map_vadd' := _}, cont := _}
@[simp]
theorem
continuous_affine_map.coe_const
(R : Type u_1)
{V : Type u_2}
{W : Type u_3}
(P : Type u_4)
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
(q : Q) :
⇑(continuous_affine_map.const R P q) = function.const P q
@[protected, instance]
noncomputable
def
continuous_affine_map.inhabited
(R : Type u_1)
{V : Type u_2}
{W : Type u_3}
(P : Type u_4)
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q] :
Equations
- continuous_affine_map.inhabited R P = {default := continuous_affine_map.const R P continuous_affine_map.inhabited._proof_1.some}
def
continuous_affine_map.comp
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
{W₂ : Type u_6}
{Q₂ : Type u_7}
[add_comm_group W₂]
[module R W₂]
[topological_space Q₂]
[add_torsor W₂ Q₂]
(f : Q →A[R] Q₂)
(g : P →A[R] Q) :
The composition of morphisms is a morphism.
@[simp, norm_cast]
theorem
continuous_affine_map.coe_comp
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
{W₂ : Type u_6}
{Q₂ : Type u_7}
[add_comm_group W₂]
[module R W₂]
[topological_space Q₂]
[add_torsor W₂ Q₂]
(f : Q →A[R] Q₂)
(g : P →A[R] Q) :
theorem
continuous_affine_map.comp_apply
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space Q]
[add_torsor W Q]
{W₂ : Type u_6}
{Q₂ : Type u_7}
[add_comm_group W₂]
[module R W₂]
[topological_space Q₂]
[add_torsor W₂ Q₂]
(f : Q →A[R] Q₂)
(g : P →A[R] Q)
(x : P) :
@[protected, instance]
def
continuous_affine_map.has_zero
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W] :
Equations
@[simp, norm_cast]
theorem
continuous_affine_map.coe_zero
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W] :
theorem
continuous_affine_map.zero_apply
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
(x : P) :
@[protected, instance]
def
continuous_affine_map.has_smul
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
{S : Type u_8}
[topological_space W]
[monoid S]
[distrib_mul_action S W]
[smul_comm_class R S W]
[has_continuous_const_smul S W] :
@[simp, norm_cast]
theorem
continuous_affine_map.coe_smul
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
{S : Type u_8}
[topological_space W]
[monoid S]
[distrib_mul_action S W]
[smul_comm_class R S W]
[has_continuous_const_smul S W]
(t : S)
(f : P →A[R] W) :
theorem
continuous_affine_map.smul_apply
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
{S : Type u_8}
[topological_space W]
[monoid S]
[distrib_mul_action S W]
[smul_comm_class R S W]
[has_continuous_const_smul S W]
(t : S)
(f : P →A[R] W)
(x : P) :
@[protected, instance]
def
continuous_affine_map.is_central_scalar
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
{S : Type u_8}
[topological_space W]
[monoid S]
[distrib_mul_action S W]
[smul_comm_class R S W]
[has_continuous_const_smul S W]
[distrib_mul_action Sᵐᵒᵖ W]
[is_central_scalar S W] :
is_central_scalar S (P →A[R] W)
@[protected, instance]
def
continuous_affine_map.mul_action
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
{S : Type u_8}
[topological_space W]
[monoid S]
[distrib_mul_action S W]
[smul_comm_class R S W]
[has_continuous_const_smul S W] :
mul_action S (P →A[R] W)
Equations
- continuous_affine_map.mul_action = function.injective.mul_action coe_fn continuous_affine_map.mul_action._proof_1 continuous_affine_map.coe_smul
@[protected, instance]
def
continuous_affine_map.has_add
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W] :
@[simp, norm_cast]
theorem
continuous_affine_map.coe_add
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W]
(f g : P →A[R] W) :
theorem
continuous_affine_map.add_apply
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W]
(f g : P →A[R] W)
(x : P) :
@[protected, instance]
def
continuous_affine_map.has_sub
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W] :
@[simp, norm_cast]
theorem
continuous_affine_map.coe_sub
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W]
(f g : P →A[R] W) :
theorem
continuous_affine_map.sub_apply
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W]
(f g : P →A[R] W)
(x : P) :
@[protected, instance]
def
continuous_affine_map.has_neg
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W] :
@[simp, norm_cast]
theorem
continuous_affine_map.coe_neg
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W]
(f : P →A[R] W) :
theorem
continuous_affine_map.neg_apply
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W]
(f : P →A[R] W)
(x : P) :
@[protected, instance]
def
continuous_affine_map.add_comm_group
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
[topological_space W]
[topological_add_group W] :
add_comm_group (P →A[R] W)
Equations
- continuous_affine_map.add_comm_group = function.injective.add_comm_group coe_fn continuous_affine_map.add_comm_group._proof_5 continuous_affine_map.coe_zero continuous_affine_map.coe_add continuous_affine_map.coe_neg continuous_affine_map.coe_sub continuous_affine_map.add_comm_group._proof_6 continuous_affine_map.add_comm_group._proof_7
@[protected, instance]
def
continuous_affine_map.distrib_mul_action
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
{S : Type u_8}
[topological_space W]
[topological_add_group W]
[monoid S]
[distrib_mul_action S W]
[smul_comm_class R S W]
[has_continuous_const_smul S W] :
distrib_mul_action S (P →A[R] W)
Equations
- continuous_affine_map.distrib_mul_action = function.injective.distrib_mul_action {to_fun := λ (f : P →A[R] W), f.to_affine_map.to_fun, map_zero' := _, map_add' := _} continuous_affine_map.distrib_mul_action._proof_2 continuous_affine_map.coe_smul
@[protected, instance]
def
continuous_affine_map.module
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
{P : Type u_4}
[ring R]
[add_comm_group V]
[module R V]
[topological_space P]
[add_torsor V P]
[add_comm_group W]
[module R W]
{S : Type u_8}
[topological_space W]
[topological_add_group W]
[semiring S]
[module S W]
[smul_comm_class R S W]
[has_continuous_const_smul S W] :
Equations
- continuous_affine_map.module = function.injective.module S {to_fun := λ (f : P →A[R] W), f.to_affine_map.to_fun, map_zero' := _, map_add' := _} continuous_affine_map.module._proof_2 continuous_affine_map.module._proof_3
def
continuous_linear_map.to_continuous_affine_map
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
[ring R]
[add_comm_group V]
[module R V]
[topological_space V]
[add_comm_group W]
[module R W]
[topological_space W]
(f : V →L[R] W) :
A continuous linear map can be regarded as a continuous affine map.
@[simp]
theorem
continuous_linear_map.coe_to_continuous_affine_map
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
[ring R]
[add_comm_group V]
[module R V]
[topological_space V]
[add_comm_group W]
[module R W]
[topological_space W]
(f : V →L[R] W) :
⇑(f.to_continuous_affine_map) = ⇑f
@[simp]
theorem
continuous_linear_map.to_continuous_affine_map_map_zero
{R : Type u_1}
{V : Type u_2}
{W : Type u_3}
[ring R]
[add_comm_group V]
[module R V]
[topological_space V]
[add_comm_group W]
[module R W]
[topological_space W]
(f : V →L[R] W) :
⇑(f.to_continuous_affine_map) 0 = 0