∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : IsUniformAddGroup β] (f : α →+ β) (hf : Continuous ⇑f),
  Continuous ⇑(f.completion hf)