mathlib3 documentation

topology.algebra.affine

Topological properties of affine spaces and maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

@[continuity]

The line map is continuous.