Topological properties of affine spaces and maps
For now, this contains only a few facts regarding the continuity of affine maps in the special case when the point space and vector space are the same.
theorem
affine_map.continuous_iff
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ring R]
[add_comm_group E]
[semimodule R E]
[topological_space E]
[add_comm_group F]
[semimodule R F]
[topological_space F]
[topological_add_group F]
{f : affine_map R E F} :
continuous ⇑f ↔ continuous ⇑(f.linear)
An affine map is continuous iff its underlying linear map is continuous.
theorem
affine_map.line_map_continuous
{R : Type u_1}
{F : Type u_3}
[ring R]
[add_comm_group F]
[semimodule R F]
[topological_space F]
[topological_add_group F]
[topological_space R]
[topological_semimodule R F]
{p v : F} :
The line map is continuous.