case h.e'_5
α : Type u_1
β : Type u_2
γ : Type ?u.162528
δ : Type ?u.162531
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
h : Continuous f
h' : ∀ (x : α), f x = g x
⊢ g = f
α : Type u_1
β : Type u_2
γ : Type ?u.162528
δ : Type ?u.162531
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
h : Continuous f
h' : ∀ (x : α), f x = g x
⊢ Continuous g
convert h
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type ?u.162528
δ : Type ?u.162531
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
h : Continuous f
h' : ∀ (x : α), f x = g x
x✝ : α
⊢ g x✝ = f x✝
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type ?u.162528
δ : Type ?u.162531
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
h : Continuous f
h' : ∀ (x : α), f x = g x
⊢ g = f
ext
no goals
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type ?u.162528
δ : Type ?u.162531
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
h : Continuous f
h' : ∀ (x : α), f x = g x
x✝ : α
⊢ g x✝ = f x✝
rw [h']