Interactions between differentiability, smoothness and manifold derivatives #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We give the relation between mdifferentiable, cont_mdiff, mfderiv, tangent_map
and related notions.
Main statements #
cont_mdiff_on.cont_mdiff_on_tangent_map_withinstates that the bundled derivative of aCⁿfunction in a domain isCᵐwhenm + 1 ≤ n.cont_mdiff.cont_mdiff_tangent_mapstates that the bundled derivative of aCⁿfunction isCᵐwhenm + 1 ≤ n.
Definition of smooth functions between manifolds #
Deducing differentiability from smoothness #
theorem
cont_mdiff_within_at.mdifferentiable_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
{n : ℕ∞}
(hf : cont_mdiff_within_at I I' n f s x)
(hn : 1 ≤ n) :
mdifferentiable_within_at I I' f s x
theorem
cont_mdiff_at.mdifferentiable_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
{n : ℕ∞}
(hf : cont_mdiff_at I I' n f x)
(hn : 1 ≤ n) :
mdifferentiable_at I I' f x
theorem
cont_mdiff_on.mdifferentiable_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{n : ℕ∞}
(hf : cont_mdiff_on I I' n f s)
(hn : 1 ≤ n) :
mdifferentiable_on I I' f s
theorem
cont_mdiff.mdifferentiable
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{n : ℕ∞}
(hf : cont_mdiff I I' n f)
(hn : 1 ≤ n) :
mdifferentiable I I' f
theorem
smooth_within_at.mdifferentiable_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
(hf : smooth_within_at I I' f s x) :
mdifferentiable_within_at I I' f s x
theorem
smooth_at.mdifferentiable_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
(hf : smooth_at I I' f x) :
mdifferentiable_at I I' f x
theorem
smooth_on.mdifferentiable_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
(hf : smooth_on I I' f s) :
mdifferentiable_on I I' f s
theorem
smooth.mdifferentiable
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
(hf : smooth I I' f) :
mdifferentiable I I' f
theorem
smooth.mdifferentiable_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{x : M}
(hf : smooth I I' f) :
mdifferentiable_at I I' f x
theorem
smooth.mdifferentiable_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : M → M'}
{s : set M}
{x : M}
(hf : smooth I I' f) :
mdifferentiable_within_at I I' f s x
The derivative of a smooth function is smooth #
theorem
cont_mdiff_at.mfderiv
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{F : Type u_8}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_9}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_10}
[topological_space N]
[charted_space G N]
[Js : smooth_manifold_with_corners J N]
{m n : ℕ∞}
{x₀ : N}
(f : N → M → M')
(g : N → M)
(hf : cont_mdiff_at (J.prod I) I' n (function.uncurry f) (x₀, g x₀))
(hg : cont_mdiff_at J I m g x₀)
(hmn : m + 1 ≤ n) :
cont_mdiff_at J (model_with_corners_self 𝕜 (E →L[𝕜] E')) m (in_tangent_coordinates I I' g (λ (x : N), f x (g x)) (λ (x : N), mfderiv I I' (f x) (g x)) x₀) x₀
The function that sends x to the y-derivative of f(x,y) at g(x) is C^m at x₀,
where the derivative is taken as a continuous linear map.
We have to assume that f is C^n at (x₀, g(x₀)) for n ≥ m + 1 and g is C^m at x₀.
We have to insert a coordinate change from x₀ to x to make the derivative sensible.
This result is used to show that maps into the 1-jet bundle and cotangent bundle are smooth.
cont_mdiff_at.mfderiv_id and cont_mdiff_at.mfderiv_const are special cases of this.
This result should be generalized to a cont_mdiff_within_at for mfderiv_within.
If we do that, we can deduce cont_mdiff_on.cont_mdiff_on_tangent_map_within from this.
theorem
cont_mdiff_at.mfderiv_const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{m n : ℕ∞}
{x₀ : M}
{f : M → M'}
(hf : cont_mdiff_at I I' n f x₀)
(hmn : m + 1 ≤ n) :
cont_mdiff_at I (model_with_corners_self 𝕜 (E →L[𝕜] E')) m (in_tangent_coordinates I I' id f (mfderiv I I' f) x₀) x₀
The derivative D_yf(y) is C^m at x₀, where the derivative is taken as a continuous
linear map. We have to assume that f is C^n at x₀ for some n ≥ m + 1.
We have to insert a coordinate change from x₀ to x to make the derivative sensible.
This is a special case of cont_mdiff_at.mfderiv where f does not contain any parameters and
g = id.
theorem
cont_mdiff_at.mfderiv_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{F : Type u_8}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_9}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_10}
[topological_space N]
[charted_space G N]
[Js : smooth_manifold_with_corners J N]
{F' : Type u_11}
[normed_add_comm_group F']
[normed_space 𝕜 F']
{G' : Type u_12}
[topological_space G']
{J' : model_with_corners 𝕜 F' G'}
{N' : Type u_13}
[topological_space N']
[charted_space G' N']
{m n : ℕ∞}
{x₀ : N'}
(f : N → M → M')
(g : N → M)
(g₁ : N' → N)
(g₂ : N' → E)
(hf : cont_mdiff_at (J.prod I) I' n (function.uncurry f) (g₁ x₀, g (g₁ x₀)))
(hg : cont_mdiff_at J I m g (g₁ x₀))
(hg₁ : cont_mdiff_at J' J m g₁ x₀)
(hg₂ : cont_mdiff_at J' (model_with_corners_self 𝕜 E) m g₂ x₀)
(hmn : m + 1 ≤ n) :
cont_mdiff_at J' (model_with_corners_self 𝕜 E') m (λ (x : N'), ⇑(in_tangent_coordinates I I' g (λ (x : N), f x (g x)) (λ (x : N), mfderiv I I' (f x) (g x)) (g₁ x₀) (g₁ x)) (g₂ x)) x₀
The function that sends x to the y-derivative of f(x,y) at g(x) applied to g₂(x) is
C^n at x₀, where the derivative is taken as a continuous linear map.
We have to assume that f is C^(n+1) at (x₀, g(x₀)) and g is C^n at x₀.
We have to insert a coordinate change from x₀ to g₁(x) to make the derivative sensible.
This is similar to cont_mdiff_at.mfderiv, but where the continuous linear map is applied to a
(variable) vector.
The tangent map of a smooth function is smooth #
theorem
cont_mdiff_on.continuous_on_tangent_map_within_aux
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{n : ℕ∞}
{f : H → H'}
{s : set H}
(hf : cont_mdiff_on I I' n f s)
(hn : 1 ≤ n)
(hs : unique_mdiff_on I s) :
continuous_on (tangent_map_within I I' f s) (bundle.total_space.proj ⁻¹' s)
If a function is C^n with 1 ≤ n on a domain with unique derivatives, then its bundled
derivative is continuous. In this auxiliary lemma, we prove this fact when the source and target
space are model spaces in models with corners. The general fact is proved in
cont_mdiff_on.continuous_on_tangent_map_within
theorem
cont_mdiff_on.cont_mdiff_on_tangent_map_within_aux
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{m n : ℕ∞}
{f : H → H'}
{s : set H}
(hf : cont_mdiff_on I I' n f s)
(hmn : m + 1 ≤ n)
(hs : unique_mdiff_on I s) :
cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s) (bundle.total_space.proj ⁻¹' s)
If a function is C^n on a domain with unique derivatives, then its bundled derivative is
C^m when m+1 ≤ n. In this auxiliary lemma, we prove this fact when the source and target space
are model spaces in models with corners. The general fact is proved in
cont_mdiff_on.cont_mdiff_on_tangent_map_within
theorem
cont_mdiff_on.cont_mdiff_on_tangent_map_within
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{m n : ℕ∞}
(hf : cont_mdiff_on I I' n f s)
(hmn : m + 1 ≤ n)
(hs : unique_mdiff_on I s) :
cont_mdiff_on I.tangent I'.tangent m (tangent_map_within I I' f s) (bundle.total_space.proj ⁻¹' s)
If a function is C^n on a domain with unique derivatives, then its bundled derivative
is C^m when m+1 ≤ n.
theorem
cont_mdiff_on.continuous_on_tangent_map_within
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{s : set M}
{n : ℕ∞}
(hf : cont_mdiff_on I I' n f s)
(hmn : 1 ≤ n)
(hs : unique_mdiff_on I s) :
continuous_on (tangent_map_within I I' f s) (bundle.total_space.proj ⁻¹' s)
If a function is C^n on a domain with unique derivatives, with 1 ≤ n, then its bundled
derivative is continuous there.
theorem
cont_mdiff.cont_mdiff_tangent_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{m n : ℕ∞}
(hf : cont_mdiff I I' n f)
(hmn : m + 1 ≤ n) :
cont_mdiff I.tangent I'.tangent m (tangent_map I I' f)
If a function is C^n, then its bundled derivative is C^m when m+1 ≤ n.
theorem
cont_mdiff.continuous_tangent_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
[I's : smooth_manifold_with_corners I' M']
{f : M → M'}
{n : ℕ∞}
(hf : cont_mdiff I I' n f)
(hmn : 1 ≤ n) :
continuous (tangent_map I I' f)
If a function is C^n, with 1 ≤ n, then its bundled derivative is continuous.
theorem
tangent_bundle.tangent_map_tangent_bundle_pure
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
[Is : smooth_manifold_with_corners I M]
(p : tangent_bundle I M) :
tangent_map I I.tangent (bundle.zero_section E (tangent_space I)) p = {proj := {proj := p.proj, snd := 0}, snd := (p.snd, 0)}
The derivative of the zero section of the tangent bundle maps ⟨x, v⟩ to ⟨⟨x, 0⟩, ⟨v, 0⟩⟩.
Note that, as currently framed, this is a statement in coordinates, thus reliant on the choice of the coordinate system we use on the tangent bundle.
However, the result itself is coordinate-dependent only to the extent that the coordinates determine a splitting of the tangent bundle. Moreover, there is a canonical splitting at each point of the zero section (since there is a canonical horizontal space there, the tangent space to the zero section, in addition to the canonical vertical space which is the kernel of the derivative of the projection), and this canonical splitting is also the one that comes from the coordinates on the tangent bundle in our definitions. So this statement is not as crazy as it may seem.
TODO define splittings of vector bundles; state this result invariantly.
@[protected]
theorem
cont_mdiff_map.mdifferentiable'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
(f : cont_mdiff_map I I' M M' n)
(hn : 1 ≤ n) :
mdifferentiable I I' ⇑f
@[protected]
theorem
cont_mdiff_map.mdifferentiable
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : cont_mdiff_map I I' M M' ⊤) :
mdifferentiable I I' ⇑f
@[protected]
theorem
cont_mdiff_map.mdifferentiable_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : cont_mdiff_map I I' M M' ⊤)
{x : M} :
mdifferentiable_at I I' ⇑f x