coordChangeL — Mathlib

English

Given a differentiable f within a subset s, and base-set membership for f x, the coordinate-change L is differentiable within s at x for the map y ↦ (f y).

Русский

Пусть f дифференцируема внутри множества s и f x принадлежит базовым множествам; тогда переход координат L дифференцируем внутри s в точке x для отображения y ↦ f(y).

LaTeX

$$$\displaystyle MDifferentiableWithinAt\! IM \, 𝓘(\mathbb{K}, F \to_L[\mathbb{K}] F) (\lambda y. (e.coordChangeL 𝕜 e' (f y) : F \to_L[\mathbb{K}] F))\; s\ x.$$$

Lean4

protected theorem coordChangeL (hf : MDifferentiable IM IB f) (he : ∀ x, f x ∈ e.baseSet)
    (he' : ∀ x, f x ∈ e'.baseSet) :
    MDifferentiable IM 𝓘(𝕜, F →L[𝕜] F) (fun y ↦ (e.coordChangeL 𝕜 e' (f y) : F →L[𝕜] F)) := fun x ↦
  (hf x).coordChangeL (he x) (he' x)

Похожие утверждения