snd — Mathlib

English

For f: M → M' × N', differentiability within s is equivalent to differentiability of Prod.fst ∘ f and Prod.snd ∘ f within s.

Русский

Для f: M → M' × N' дифференцируемость внутри s эквивалентна дифференцируемости Prod.fst ∘ f и Prod.snd ∘ f внутри s.

LaTeX

$$$\mathrm{MDifferentiableWithinAt}\, I\ (I'.prod J')\, f\, s\, x \iff \mathrm{MDifferentiableWithinAt}\, I\ I' (\mathrm{Prod.fst} \circ f) \ s \ x \land \mathrm{MDifferentiableWithinAt}\, I\ J' (\mathrm{Prod.snd} \circ f) \ s \ x$$$

Lean4

theorem snd {f : N → M × M'} {s : Set N} {x : N} (hf : MDifferentiableWithinAt J (I.prod I') f s x) :
    MDifferentiableWithinAt J I' (fun x => (f x).2) s x :=
  mdifferentiableAt_snd.comp_mdifferentiableWithinAt x hf

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