contDiffWithinAtProp_mono_of_mem_nhdsWithin

English

Equality of ContDiffWithinAtProp under self model; equivalence with ContDiffWithinAt on identity model.

Русский

Сопоставление ContDiffWithinAtProp через self модель; эквивалентно ContDiffWithinAt на идентичной модели.

LaTeX

$$$ ContDiffWithinAtProp (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x \iff ContDiffWithinAt 𝕜 n f s x $$$

Lean4

theorem contDiffWithinAtProp_mono_of_mem_nhdsWithin (n : WithTop ℕ∞) ⦃s x t⦄ ⦃f : H → H'⦄ (hts : s ∈ 𝓝[t] x)
    (h : ContDiffWithinAtProp I I' n f s x) : ContDiffWithinAtProp I I' n f t x :=
  by
  refine h.mono_of_mem_nhdsWithin ?_
  refine inter_mem ?_ (mem_of_superset self_mem_nhdsWithin inter_subset_right)
  rwa [← Filter.mem_map, ← I.image_eq, I.symm_map_nhdsWithin_image]

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