contDiffOn_restrContDiff_source — Mathlib

English

Restriction of a patch to its source retains ContDiffOn when n is finite.

Русский

Ограничение частичной гомеоморфии до источника сохраняет ContDiffOn при конечном n.

LaTeX

$$$\text{OpenPartialHomeomorph.contDiffOn_restrContDiff_source} \; (f : OpenPartialHomeomorph E F) {n} (hn : Ne n (WithTop.some instTopENat.top)) :\n ContDiffOn 𝕜 n f (OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).source$$$

Lean4

theorem contDiffOn_restrContDiff_source (f : OpenPartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ∞) :
    ContDiffOn 𝕜 n f (f.restrContDiff 𝕜 n hn).source := fun _x hx ↦ hx.2.1.contDiffWithinAt

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