mdifferentiableOn_fst — Mathlib

English

For any sets s ⊆ M × M′, the first projection is differentiable on s in the MF sense: MDifferentiableOn (I.prod I′) I Prod.fst s.

Русский

Для любых множеств s ⊆ M × M′ первая проекция дифференцируема на s в MF-терминах: MDifferentiableOn (I.prod I′) I Prod.fst s.

LaTeX

$$$\mathrm{MDifferentiableOn}(I\prod I',\,I,\,Prod.fst\,s)$$$

Lean4

theorem mdifferentiableOn_fst {s : Set (M × M')} : MDifferentiableOn (I.prod I') I Prod.fst s :=
  mdifferentiable_fst.mdifferentiableOn

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