mathlib documentation


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] [module R E] [topological_space E] [add_comm_group F] [module R F] [topological_space F] [topological_add_group F] {f : E →ᵃ[R] F} :

An affine map is continuous iff its underlying linear map is continuous.

The line map is continuous.