nndist_eq_iSup — Mathlib

English

When p = ∞, the distance in PiLp is the supremum over coordinates: nndist x y = sup_i nndist (x_i) (y_i).

Русский

Когда p = ∞, расстояние в PiLp равно супремуму по координатам: nndist x y = sup_i nndist (x_i) (y_i).

LaTeX

$$nndist x y = ⨆ i, nndist (x i) (y i)$$

Lean4

theorem nndist_eq_iSup {β : ι → Type*} [∀ i, PseudoMetricSpace (β i)] (x y : PiLp ∞ β) :
    nndist x y = ⨆ i, nndist (x i) (y i) :=
  NNReal.eq <| by
    push_cast
    exact dist_eq_iSup _ _

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