funProp minimal setup for Differentiable(At/On) #
theorem
differentiableOn_id'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{s : Set E}
:
DifferentiableOn K (fun (x : E) => x) s
theorem
Differentiable.comp'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace K F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace K G]
{f : E → F}
{g : F → G}
(hg : Differentiable K g)
(hf : Differentiable K f)
:
Differentiable K fun (x : E) => g (f x)
theorem
DifferentiableAt.comp'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace K F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace K G]
{x : E}
{f : E → F}
{g : F → G}
(hg : DifferentiableAt K g (f x))
(hf : DifferentiableAt K f x)
:
DifferentiableAt K (fun (x : E) => g (f x)) x
theorem
DifferentiableOn.comp'
{K : Type u_1}
[NontriviallyNormedField K]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace K E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace K F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace K G]
{f : E → F}
{s : Set E}
{g : F → G}
{t : Set F}
(hg : DifferentiableOn K g t)
(hf : DifferentiableOn K f s)
(st : Set.MapsTo f s t)
:
DifferentiableOn K (fun (x : E) => g (f x)) s