English
There is a natural metric space structure on the completion of a pseudo-metric space α, making Completion α a metric space with the usual distance.
Русский
У завершения псевдометрического пространства α имеется естественная метрическая структура; Completion α является метрическим пространством с обычным расстоянием.
LaTeX
$$$\text{MetricSpace}(\mathrm{Completion}\;\alpha)$$$
Lean4
instance {M} [Zero M] [Zero α] [SMul M α] [PseudoMetricSpace M] [IsBoundedSMul M α] : IsBoundedSMul M (Completion α)
where
dist_smul_pair' c x₁
x₂ := by
induction x₁, x₂ using induction_on₂ with
| hp =>
exact
isClosed_le ((continuous_fst.const_smul _).dist (continuous_snd.const_smul _))
(continuous_const.mul (continuous_fst.dist continuous_snd))
| ih x₁ x₂ =>
rw [← coe_smul, ← coe_smul, Completion.dist_eq, Completion.dist_eq]
exact dist_smul_pair c x₁ x₂
dist_pair_smul' c₁ c₂
x := by
induction x using induction_on with
| hp =>
exact
isClosed_le ((continuous_const_smul _).dist (continuous_const_smul _))
(continuous_const.mul (continuous_id.dist continuous_const))
| ih x =>
rw [← coe_smul, ← coe_smul, Completion.dist_eq, ← coe_zero, Completion.dist_eq]
exact dist_pair_smul c₁ c₂ x
