Smooth affine maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains results about smoothness of affine maps.
Main definitions: #
continuous_affine_map.cont_diff: a continuous affine map is smooth
theorem
continuous_affine_map.cont_diff
{𝕜 : Type u_1}
{V : Type u_2}
{W : Type u_3}
[nontrivially_normed_field 𝕜]
[normed_add_comm_group V]
[normed_space 𝕜 V]
[normed_add_comm_group W]
[normed_space 𝕜 W]
{n : ℕ∞}
(f : V →A[𝕜] W) :
A continuous affine map between normed vector spaces is smooth.