comp_inter — Mathlib

English

If hf : ContDiffOn 𝕜 n f s and hg : ContDiffOn 𝕜 n g s, then ContDiffOn 𝕜 n (x ↦ (f x, g x)) s.

Русский

Если f и g — C^n на s в области, тогда пара (f,g) — C^n на s.

LaTeX

$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f\,s \land \operatorname{ContDiffOn}_{\mathbb{K}}^{n} g\,s \Rightarrow \operatorname{ContDiffOn}_{\mathbb{K}}^{n} (\lambda x. (f x, g x))\,s$$$

Lean4

/-- The composition of `C^n` functions on domains is `C^n`. -/
theorem comp_inter {s : Set E} {t : Set F} {g : F → G} {f : E → F} (hg : ContDiffOn 𝕜 n g t) (hf : ContDiffOn 𝕜 n f s) :
    ContDiffOn 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) :=
  hg.comp (hf.mono inter_subset_left) inter_subset_right

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