English
If f and g are equal on a set s, and both are continuous on a larger set t with s ⊆ t ⊆ closure s, then f and g are equal on all of t.
Русский
Если функции f и g равны на множестве s, и обе непрерывны на большем множестве t с условием s ⊆ t ⊆ closure s, тогда f и g равны на всём t.
LaTeX
$$$\\text{If } s,t\\subseteq X,\\; f,g:X\\to Y,\\; h: \\; f=g\\text{ on } s,\\; \\text{ContinuousOn}(f,t),\\; \\text{ContinuousOn}(g,t),\\; s\\subseteq t,\\; t\\subseteq \\overline{s} \\Rightarrow f=g\\text{ on }t.$$$
Lean4
/-- If `f x = g x` for all `x ∈ s` and `f`, `g` are continuous on `t`, `s ⊆ t ⊆ closure s`, then
`f x = g x` for all `x ∈ t`. See also `Set.EqOn.closure`. -/
theorem of_subset_closure [T2Space Y] {s t : Set X} {f g : X → Y} (h : EqOn f g s) (hf : ContinuousOn f t)
(hg : ContinuousOn g t) (hst : s ⊆ t) (hts : t ⊆ closure s) : EqOn f g t :=
by
intro x hx
have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)
exact
tendsto_nhds_unique_of_eventuallyEq ((hf x hx).mono_left <| nhdsWithin_mono _ hst)
((hg x hx).mono_left <| nhdsWithin_mono _ hst) (h.eventuallyEq_of_mem self_mem_nhdsWithin)
