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.

TODO: Deal with the case where the point spaces are different from the vector spaces. Note that we do have some results in this direction under the assumption that the topologies are induced by (semi)norms.

theorem affine_map.continuous_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [add_comm_group E] [topological_space E] [add_comm_group F] [topological_space F] [topological_add_group F] [ring R] [module R E] [module R F] {f : E →ᵃ[R] F} :

An affine map is continuous iff its underlying linear map is continuous. See also affine_map.continuous_linear_iff.


The line map is continuous.

theorem affine_map.homothety_is_open_map {R : Type u_1} {F : Type u_3} [add_comm_group F] [topological_space F] [topological_add_group F] [field R] [module R F] [has_continuous_const_smul R F] (x : F) (t : R) (ht : t 0) :