dist_ofDual — Mathlib

English

Let X be a metric space. For any a, b in the order dual X^op, the distance between their images in X^op equals the distance between a and b in X. In symbols, dist(ofDual(a), ofDual(b)) = dist(a, b).

Русский

Пусть X — метрическое пространство. Для любых a, b из порядка-двойственности X^op расстояние между образами a и b в X^op равно расстоянию между a и b в X: dist(ofDual(a), ofDual(b)) = dist(a, b).

LaTeX

$$$\operatorname{dist}(\operatorname{ofDual} a, \operatorname{ofDual} b) = \operatorname{dist}(a,b)$$$

Lean4

@[simp]
theorem dist_ofDual (a b : Xᵒᵈ) : dist (ofDual a) (ofDual b) = dist a b :=
  rfl

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