Documentation

Mathlib.Analysis.Calculus.AddTorsor.AffineMap

Smooth affine maps #

This file contains results about smoothness of affine maps.

Main definitions: #

theorem ContinuousAffineMap.contDiff {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] {n : ℕ∞} (f : V →ᴬ[𝕜] W) :
ContDiff 𝕜 n f

A continuous affine map between normed vector spaces is smooth.