eq_of_nhdsWithin — Mathlib

English

If f equals g eventually with respect to 𝓝[s] a and a ∈ s, then f a = g a.

Русский

Если f и g совпадают почти повсеместно относительно 𝓝[s] a и a ∈ s, то f(a) = g(a).

LaTeX

$$$ (f =^\\!=[\\! 𝓝[s] a] g) \\rightarrow a \in s \\rightarrow f a = g a $$$

Lean4

theorem eq_of_nhdsWithin {s : Set α} {f g : α → β} {a : α} (h : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : f a = g a :=
  h.self_of_nhdsWithin hmem

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