English
The tangent bundle of a product is canonically isomorphic to the product of tangent bundles; the isomorphism sends a tangent vector to its pair of component tangent vectors.
Русский
Буров tangent bundle произведения есть каноническое изоморфизм с произведением касательных проб, компонентные вектора переходят парами.
LaTeX
$$$\mathrm{equiv\_TangentBundleProd} : TangentBundle (I\.prod I') (M \times M') \cong (TangentBundle I M) \times (TangentBundle I' M')$$$
Lean4
/-- 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 `ContMDiffAt.mfderiv`, but where the continuous linear map is applied to a
(variable) vector.
-/
theorem mfderiv_apply {x₀ : N'} (f : N → M → M') (g : N → M) (g₁ : N' → N) (g₂ : N' → E)
(hf : ContMDiffAt (J.prod I) I' n (Function.uncurry f) (g₁ x₀, g (g₁ x₀))) (hg : ContMDiffAt J I m g (g₁ x₀))
(hg₁ : ContMDiffAt J' J m g₁ x₀) (hg₂ : ContMDiffAt J' 𝓘(𝕜, E) m g₂ x₀) (hmn : m + 1 ≤ n) :
ContMDiffAt J' 𝓘(𝕜, E') m
(fun x =>
inTangentCoordinates I I' g (fun x => f x (g x)) (fun x => mfderiv I I' (f x) (g x)) (g₁ x₀) (g₁ x) (g₂ x))
x₀ :=
((hf.mfderiv f g hg hmn).comp_of_eq hg₁ rfl).clm_apply hg₂
