nndist_ofDual — Mathlib

English

For elements a,b in the dual space X^op, the distance between ofDual a and ofDual b equals the distance between a and b.

Русский

Для элементов a,b типа X^op расстояние между ofDual a и ofDual b равно расстоянию между a и b.

LaTeX

$$$\mathrm{nndist}(\mathrm{ofDual}(a),\mathrm{ofDual}(b)) = \mathrm{nndist}(a,b)$$$

Lean4

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

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