mono_nhds — Mathlib

English

If hs has the unique MDiff property at s and nhdsWithin x s is mapped into nhdsWithin x t, then the unique MDiff property holds for t as well.

Русский

Если для s есть уникальная MDiff и nhdsWithin x s отображается в nhdsWithin x t, то свойство сохраняется для t.

LaTeX

$$UniqueMDiffWithinAt I t x, given hs : UniqueMDiffWithinAt I s x and ht : nhdsWithin x s ≤ nhdsWithin x t$$

Lean4

nonrec theorem mono_nhds {s t : Set M} {x : M} (hs : UniqueMDiffWithinAt I s x) (ht : 𝓝[s] x ≤ 𝓝[t] x) :
    UniqueMDiffWithinAt I t x :=
  hs.mono_nhds <| by simpa only [← map_extChartAt_nhdsWithin] using Filter.map_mono ht

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