instMetricSpace — Mathlib

English

Let α be a metric space. Endow the opposite type αᵐᵒᵖ with the metric defined by d(p, q) = d(unop(p), unop(q)). This makes αᵐᵒᵖ a metric space, and the unop map is an isometry.

Русский

Пусть α — метрическое пространство. На противоположном типе αᵐᵒᵖ задаётся метрика d(p, q) = d_α(unop(p), unop(q)). Это превращает αᵐᵒᵖ в метрическое пространство, а отображение unop — изометрия.

LaTeX

$$$\\operatorname{dist}_{\\alpha^{\\mathrm{op}}}(p,q)=\\operatorname{dist}_{\\alpha}(\\operatorname{unop}(p),\\operatorname{unop}(q))$$$

Lean4

@[to_additive]
instance instMetricSpace {α : Type*} [MetricSpace α] : MetricSpace αᵐᵒᵖ :=
  MetricSpace.induced MulOpposite.unop MulOpposite.unop_injective ‹_›

Похожие утверждения