mdifferentiable_snd — Mathlib

English

For s ⊆ M × M′ and x ∈ s, the function Prod.snd is MF-differentiable within s: MDifferentiableWithinAt (I.prod I′) I' Prod.snd s x.

Русский

Для множества s и точки x ∈ s функция Prod.snd дифференцируема внутри s в MF- sense.

LaTeX

$$$\mathrm{MDifferentiableWithinAt}(I\prod I',\,I',\,\mathrm{Prod.snd},\,s,\,x)$$$

Lean4

theorem mdifferentiable_snd : MDifferentiable (I.prod I') I' (Prod.snd : M × M' → M') := fun _ => mdifferentiableAt_snd

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