English
The product map of two C^n functions on a set is C^n on the product set.
Русский
Произведение двух функций класса C^n на множестве является C^n на произведении множеств.
LaTeX
$$$\\forall {E'},{F'},\\; \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ f\\ s \\to \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ g\\ t \\to \\mathrm{ContDiffOn}_{\\mathbb{k}}\\ n\\ (\\mathrm{Prod.map}\\ f\\ g)\\ (s\\timesˢ t)$$$
Lean4
/-- In a complete normed algebra, the operation of inversion is `C^n`, for all `n`, at each
invertible element, as it is analytic. -/
@[fun_prop]
theorem contDiffAt_ringInverse [HasSummableGeomSeries R] (x : Rˣ) : ContDiffAt 𝕜 n Ring.inverse (x : R) :=
by
have :=
AnalyticOnNhd.contDiffOn (analyticOnNhd_inverse (𝕜 := 𝕜) (A := R)) (n := n) Units.isOpen.uniqueDiffOn x x.isUnit
exact this.contDiffAt (Units.isOpen.mem_nhds x.isUnit)
