α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.126302
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Set β
f g : β → α
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
x : β
hx : x ∈ t
⊢ f x = g x
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.126302
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Set β
f g : β → α
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
⊢ EqOn f g t
intro x hx
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.126302
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Set β
f g : β → α
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
x : β
hx : x ∈ t
this : NeBot (𝓝[s] x)
⊢ f x = g x
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.126302
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Set β
f g : β → α
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
x : β
hx : x ∈ t
⊢ f x = g x
have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)
no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.126302
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Set β
f g : β → α
h : EqOn f g s
hf : ContinuousOn f t
hg : ContinuousOn g t
hst : s ⊆ t
hts : t ⊆ closure s
x : β
hx : x ∈ t
this : NeBot (𝓝[s] x)
⊢ f x = g x
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)