congr_iff_nhdsWithin — Mathlib

English

If s and t are nhdsWithin-equivalent, then P f s x ↔ P f t x.

Русский

Если s и t эквивалентны относительно nhdsWithin, то P f s x эквивалентно P f t x.

LaTeX

$$$P f s x \iff P f t x$ given (nhdsWithin x s) ≡ (nhdsWithin x t)$$

Lean4

theorem congr_iff_nhdsWithin {s : Set H} {x : H} {f g : H → H'} (h1 : f =ᶠ[𝓝[s] x] g) (h2 : f x = g x) :
    P f s x ↔ P g s x := by
  simp_rw [hG.is_local_nhds h1]
  exact ⟨hG.congr_of_forall (fun y hy ↦ hy.2) h2, hG.congr_of_forall (fun y hy ↦ hy.2.symm) h2.symm⟩

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