∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : Semiring R₁] [inst_3 : Module R₁ α] [inst_4 : Semiring R₂] [inst_5 : UniformSpace β]
  [inst_6 : AddCommGroup β] [inst_7 : Module R₂ β] {σ : R₁ →+* R₂} (f : α →SL[σ] β),
  Continuous (UniformSpace.Completion.map ⇑(↑f).toAddMonoidHom)