eq_of_nhds

Mathlib.Topology.Neighborhoods

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyEq.eq_of_nhds

English

If f and g are eventually equal in nhds x, then f(x) = g(x).

Русский

Если функции f и g равны в окрестности x, то f(x) = g(x).

LaTeX

$$$(\\nhds x).EventuallyEq f g \\Rightarrow f(x) = g(x).$$$

Lean4

theorem eq_of_nhds {f g : X → α} (h : f =ᶠ[𝓝 x] g) : f x = g x :=
  h.self_of_nhds

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru