uniqueDiffWithinAt_congr — Mathlib

English

If the neighborhood within s is equal to the neighborhood within t (nhdsWithin x s = nhdsWithin x t), then the property UniqueDiffWithinAt 𝕜 s x holds for s if and only if it holds for t.

Русский

Если окрестности в x, ограниченные s и t, совпадают, то свойство уникального различия внутри s сохраняется для s и эквивалентно этому свойству для t.

LaTeX

$$$\\forall x\\, s,t\\subseteq E,\\; 𝓝_s(x) = 𝓝_t(x) \\Rightarrow \n(\\mathrm{UniqueDiffWithinAt}_\\mathbb{K}(s,x) \\iff \\mathrm{UniqueDiffWithinAt}_\\mathbb{K}(t,x))$$$

Lean4

theorem uniqueDiffWithinAt_congr (st : 𝓝[s] x = 𝓝[t] x) : UniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x :=
  ⟨fun h => h.mono_nhds <| le_of_eq st, fun h => h.mono_nhds <| le_of_eq st.symm⟩

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