self_of_nhdsSet

Mathlib.Topology.NhdsSet

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

English

If f and g are equal eventually on 𝓝ˢ s, then f and g are equal on s.

Русский

Если функции f и g равны на 𝓝ˢ s почти повсюду, то они равны на s.

LaTeX

$$$ (f =^\![𝓝ˢ s] g) \Rightarrow (\forall x \in s, f(x) = g(x)) $$$

Lean4

nonrec theorem self_of_nhdsSet {Y} {f g : X → Y} (h : f =ᶠ[𝓝ˢ s] g) : EqOn f g s :=
  h.self_of_nhdsSet

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

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

Разделы

Аффилиация

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