eventuallyEq_nhdsWithin_iff — Mathlib

English

For f,g : α → β, s ⊆ α, a ∈ α, f and g are equal eventually on nhdsWithin a s iff they are equal eventually on nhds a at all points of s.

Русский

Для функций f,g: α→β, множества s ⊆ α, точки a ∈ α, равенство на nhdsWithin a s эквивалентно равенству на nhds a на всех точках s.

LaTeX

$$$$ f =^\\!_{\\\\mathcal{N}_{[s]} a} g \\\\iff \\\\forall^\\! x \\\\in \\\\mathcal{N}_a, x \\in s \\rightarrow f x = g x. $$$$

Lean4

theorem eventuallyEq_nhdsWithin_iff {f g : α → β} {s : Set α} {a : α} :
    f =ᶠ[𝓝[s] a] g ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x :=
  mem_inf_principal

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