contDiffWithinAt_localInvariantProp

English

Monotonicity of the local invariant property under nhds inclusion.

Русский

Гладкость локальной инвариантности сохраняется при включении множеств внутрь окрестностей.

LaTeX

$$$ (nhdsWithin x t) \ni s \Rightarrow (h : ContDiffWithinAtProp I I' n f s x) \Rightarrow (ContDiffWithinAtProp I I' n f t x) $$$

Lean4

/-- Being `Cⁿ` in the model space is a local property, invariant under `C^n` maps. Therefore,
it lifts nicely to manifolds. -/
theorem contDiffWithinAt_localInvariantProp (n : WithTop ℕ∞) :
    (contDiffGroupoid n I).LocalInvariantProp (contDiffGroupoid n I') (ContDiffWithinAtProp I I' n) :=
  contDiffWithinAt_localInvariantProp_of_le n n le_rfl

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