contMDiffOn_of_mem_contDiffGroupoid

English

An element e' of the C^n-differentiable groupoid contDiffGroupoid n I is C^n on its source domain with respect to I.

Русский

Элемент e' из группы contDiffGroupoid n I является C^n на своей области определения относительно I.

LaTeX

$$$e' \\in \\mathrm{contDiffGroupoid}_n I \\quad \\Rightarrow \\quad \\mathrm{ContMDiffOn} I I n\, e' \\, e'.source.$$$

Lean4

/-- An element of `contDiffGroupoid n I` is `C^n`. -/
theorem contMDiffOn_of_mem_contDiffGroupoid {e' : OpenPartialHomeomorph H H} (h : e' ∈ contDiffGroupoid n I) :
    ContMDiffOn I I n e' e'.source :=
  (contDiffWithinAt_localInvariantProp n).liftPropOn_of_mem_groupoid contDiffWithinAtProp_id h

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