English
Two continuous maps into a Hausdorff space that agree away from a point agree in a neighborhood of that point.
Русский
Две непрерывные отображения в Хаусдорфовоe пространство, совпадающие вне точки, совпадают в окрестности этой точки.
LaTeX
$$$[T2Space Y] {x:X} {f,g:X\\to Y}\\; (hf:ContinuousAt f x)(hg:ContinuousAt g x)\\Rightarrow (f = g)\\text{ in a punctured nbhd of } x \\iff f=g\\text{ in nbhd of } x.$$$
Lean4
/-- **Local identity principle** for continuous maps: Two continuous maps into a Hausdorff space
agree in a punctured neighborhood of a non-isolated point iff they agree in a neighborhood. -/
theorem eventuallyEq_nhds_iff_eventuallyEq_nhdsNE [T2Space Y] {x : X} {f g : X → Y} (hf : ContinuousAt f x)
(hg : ContinuousAt g x) [(𝓝[≠] x).NeBot] : f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g :=
by
constructor <;> intro hfg
· apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE hfg
by_contra hCon
obtain ⟨a, ha⟩ : {x | f x ≠ g x ∧ f x = g x}.Nonempty :=
by
have h₁ := (eventually_nhdsWithin_of_eventually_nhds ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
have h₂ : ∅ ∉ 𝓝[≠] x := by exact empty_notMem (𝓝[≠] x)
simp_all
simp at ha
· exact hfg.filter_mono nhdsWithin_le_nhds
