mathlib3 documentation


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: #

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) :
cont_diff 𝕜 n f

A continuous affine map between normed vector spaces is smooth.