prod_nndist_eq_sup — Mathlib

English

For p = ∞, the distance on WithLp ∞ (α × β) satisfies nndist x y = sup{ nndist x.fst y.fst, nndist x.snd y.snd }.

Русский

При p = ∞ расстояние на WithLp ∞ (α × β) удовлетворяет: nndist x y = sup{ nndist x.fst y.fst, nndist x.snd y.snd }.

LaTeX

$$$ nndist x y = nndist x.fst y.fst \\; \\sqcup \\; nndist x.snd y.snd. $$$

Lean4

theorem prod_nndist_eq_sup [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp ∞ (α × β)) :
    nndist x y = nndist x.fst y.fst ⊔ nndist x.snd y.snd :=
  NNReal.eq <| by
    push_cast
    exact prod_dist_eq_sup _ _

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