contMDiffAt_subtype_iff — Mathlib

English

The contMDiffAt on a subtype corresponds to contMDiffAt on the ambient space via the subtype embedding.

Русский

ContMDiffAt на подпространстве соответствует ContMDiffAt на окружающем пространстве через вложение подпредставления.

LaTeX

$$ContMDiffAt_I_I'_n (fun x:U => f x) x ↔ ContMDiffAt_I_I'_n f x$$

Lean4

theorem contMDiffAt_subtype_iff {n : WithTop ℕ∞} {U : Opens M} {f : M → M'} {x : U} :
    ContMDiffAt I I' n (fun x : U ↦ f x) x ↔ ContMDiffAt I I' n f x :=
  ((contDiffWithinAt_localInvariantProp n).liftPropAt_iff_comp_subtype_val _ _).symm

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