mono_of_mem_nhdsWithin — Mathlib

English

If f is C^n within s at x, and s is contained in t in a neighborhood of x, then f is C^n within t at x.

Русский

Если функция f C^n внутри множества s в точке x, и s ⊆ t в окрестности x, то f C^n внутри t в x.

LaTeX

$$$ ContMDiffWithinAt I I' n f s x \rightarrow (s \subseteq t) \Rightarrow ContMDiffWithinAt I I' n f t x $$$

Lean4

theorem mono_of_mem_nhdsWithin (hf : ContMDiffWithinAt I I' n f s x) (hts : s ∈ 𝓝[t] x) :
    ContMDiffWithinAt I I' n f t x :=
  StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono_of_mem_nhdsWithin
    (contDiffWithinAtProp_mono_of_mem_nhdsWithin n) hf hts

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