English
Let f be a map between normed spaces and x a point. If f is C^n in the sense of ContDiffWithinAt on a set s at x, then for every subset t of s, f is also C^n on t at x.
Русский
Пусть f: E → F и точка x ∈ E. Если f имеет класс C^n в смысле ContDiffWithinAt на множество s в точке x, то для любого подмножества t ⊆ s функция f также принадлежит к тому же классу C^n на t в точке x.
LaTeX
$$$\forall {s,t : Set\,E} \; (t \subseteq s) \; \forall {f : E \to F} \; \forall {x : E} \; \forall {n : WithTop \ ENat},\; (ContDiffWithinAt 𝕜 n f s x \Rightarrow ContDiffWithinAt 𝕜 n f t x)$$$
Lean4
theorem mono (h : ContDiffWithinAt 𝕜 n f s x) {t : Set E} (hst : t ⊆ s) : ContDiffWithinAt 𝕜 n f t x :=
h.mono_of_mem_nhdsWithin <| Filter.mem_of_superset self_mem_nhdsWithin hst
