α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
a : α
⊢ DenseInducing.extend (_ : DenseInducing pureCauchy) f (pureCauchy a) = f a
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
a : α
⊢ extend f (pureCauchy a) = f a
rw [extend, if_pos hf]
no goals
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
a : α
⊢ DenseInducing.extend (_ : DenseInducing pureCauchy) f (pureCauchy a) = f a
exact uniformly_extend_of_ind uniformInducing_pureCauchy denseRange_pureCauchy hf _