α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (coe pkg a)
⊢ ∀ (a : α), AbstractCompletion.extend pkg f (coe pkg a) = g (coe pkg a)
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (coe pkg a)
⊢ AbstractCompletion.extend pkg f = g
apply pkg.funext pkg.continuous_extend hg.continuous
no goals
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
f : α → β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (coe pkg a)
⊢ ∀ (a : α), AbstractCompletion.extend pkg f (coe pkg a) = g (coe pkg a)
simpa only [pkg.extend_coe hf] using h