mono_of_mem_nhdsWithin — Mathlib

English

A corollary variant: if nhdsWithin x s ≤ nhdsWithin x t, then UniqueMDiffWithinAt I t x holds given UniqueMDiffWithinAt I s x.

Русский

Следствие: если nhdsWithin x s ≤ nhdsWithin x t, то при наличии UniqueMDiffWithinAt I s x выполняется UniqueMDiffWithinAt I t x.

LaTeX

$$UniqueMDiffWithinAt I s x → nhdsWithin x s ≤ nhdsWithin x t → UniqueMDiffWithinAt I t x$$

Lean4

theorem mono_of_mem_nhdsWithin {s t : Set M} {x : M} (hs : UniqueMDiffWithinAt I s x) (ht : t ∈ 𝓝[s] x) :
    UniqueMDiffWithinAt I t x :=
  hs.mono_nhds (nhdsWithin_le_iff.2 ht)

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