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.
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} :
continuous ⇑f ↔ continuous ⇑(f.linear)
An affine map is continuous iff its underlying linear map is continuous. See also
affine_map.continuous_linear_iff.
@[continuity]
theorem
affine_map.line_map_continuous
{R : Type u_1}
{F : Type u_3}
[add_comm_group F]
[topological_space F]
[topological_add_group F]
[ring R]
[module R F]
[topological_space R]
[has_continuous_smul R F]
{p v : F} :
The line map is continuous.
@[continuity]
theorem
affine_map.homothety_continuous
{R : Type u_1}
{F : Type u_3}
[add_comm_group F]
[topological_space F]
[topological_add_group F]
[comm_ring R]
[module R F]
[has_continuous_const_smul R F]
(x : F)
(t : R) :
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) :