dist_eq — Mathlib

English

In TopologicalSpace.Opens.CompleteCopy, the distance is given by the same sum with infDist terms translated to the open subset boundary.

Русский

В TopologicalSpace.Opens.CompleteCopy расстояние задано как та же сумма сinfDist-пределами на границе открытого подпространства.

LaTeX

$$$$\\\\dist_{s}(x,y)=dist x.1 y.1 + |1/infDist x.1 s^c - 1/infDist y.1 s^c|.$$$$

Lean4

theorem dist_eq (x y : CompleteCopy s) : dist x y = dist x.1 y.1 + abs (1 / infDist x.1 sᶜ - 1 / infDist y.1 sᶜ) :=
  rfl

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