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 AffineMap.continuous_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [TopologicalAddGroup F] [Ring R] [Module R E] [Module R F] {f : E →ᵃ[R] F} : Continuous ↑f ↔ Continuous ↑f.linear

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

theorem AffineMap.lineMap_continuous {R : Type u_1} {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [TopologicalAddGroup F] [Ring R] [Module R F] [TopologicalSpace R] [ContinuousSMul R F] {p : F} {v : F} : Continuous ↑(AffineMap.lineMap p v)

The line map is continuous.

theorem AffineMap.homothety_continuous {R : Type u_1} {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [TopologicalAddGroup F] [CommRing R] [Module R F] [ContinuousConstSMul R F] (x : F) (t : R) : Continuous ↑(AffineMap.homothety x t)

theorem AffineMap.homothety_isOpenMap {R : Type u_1} {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [TopologicalAddGroup F] [Field R] [Module R F] [ContinuousConstSMul R F] (x : F) (t : R) (ht : t ≠ 0) : IsOpenMap ↑(AffineMap.homothety x t)