comp_diffContOnCl — Mathlib

English

If f is differentiable and g is differentiable on t, then f ∘ g is differentiable on t.

Русский

Если f дифференцируема, а g дифференцируема на t, то f ∘ g дифференцируема на t.

LaTeX

$$$\text{If } hf: \text{Differentiable }\, 𝕜\, f \text{ and } hg: \text{DiffContOnCl }𝕜\, g\, t, \text{ then } \text{DiffContOnCl}(𝕜, f \circ g, t).$$$

Lean4

theorem comp_diffContOnCl {g : G → E} {t : Set G} (hf : Differentiable 𝕜 f) (hg : DiffContOnCl 𝕜 g t) :
    DiffContOnCl 𝕜 (f ∘ g) t :=
  hf.diffContOnCl.comp hg (mapsTo_image _ _)

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