comp — Mathlib

English

Same as above: differentiability is stable under composition for differentiable-on predicates.

Русский

То же самое: дифференцируемость сохраняется под композицию для предикатов дифференцируемости на множестве.

LaTeX

$$$$ \text{DifferentiableOn}_{\mathbb{K}} g t \to \text{DifferentiableOn}_{\mathbb{K}} f s \to \text{MapsTo } f s t \to \text{DifferentiableOn}_{\mathbb{K}} (g \circ f) s. $$$$

Lean4

@[fun_prop]
theorem comp {g : F → G} {t : Set F} (hg : DifferentiableOn 𝕜 g t) (hf : DifferentiableOn 𝕜 f s) (st : MapsTo f s t) :
    DifferentiableOn 𝕜 (g ∘ f) s := fun x hx => DifferentiableWithinAt.comp x (hg (f x) (st hx)) (hf x hx) st

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