English
If M acts on α by a bounded scalar multiplication (IsBoundedSMul M α), and α is a pseudo-metric space, then Completion α carries a natural IsBoundedSMul M structure extending the action.
Русский
Если M действует на α скалярным умножением, ограниченным по норме (IsBoundedSMul M α), и α — псевдометрическое пространство, то завершение α наследует структуру IsBoundedSMul M, расширяющую действие.
LaTeX
$$$\text{IsBoundedSMul } M (\mathrm{Completion}\;\alpha)$$$
Lean4
/-- Metric space structure on the completion of a pseudo_metric space. -/
instance instMetricSpace : MetricSpace (Completion α) :=
@MetricSpace.ofT0PseudoMetricSpace _
{ dist_self := Completion.dist_self
dist_comm := Completion.dist_comm
dist_triangle := Completion.dist_triangle
dist := dist
toUniformSpace := inferInstance
uniformity_dist := Completion.uniformity_dist } _
