α : Type u_2
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_1
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ DenseInducing.extend (_ : DenseInducing pkg.coe) f (coe pkg a) = f a
α : Type u_2
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_1
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ AbstractCompletion.extend pkg f (coe pkg a) = f a
rw [pkg.extend_def hf]
no goals
α : Type u_2
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_1
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ DenseInducing.extend (_ : DenseInducing pkg.coe) f (coe pkg a) = f a
exact pkg.denseInducing.extend_eq hf.continuous a