nndist_snd_le — Mathlib

English

The nonnegative distance of the second coordinates is dominated by the product distance.

Русский

Нормированное расстояние второй координаты доминирует над расстоянием продукта.

LaTeX

$$$ nndist x.snd y.snd \\le nndist x y $$$

Lean4

theorem nndist_snd_le [PseudoMetricSpace α] [PseudoMetricSpace β] (x y : WithLp p (α × β)) :
    nndist x.snd y.snd ≤ nndist x y := by simpa [← coe_nnreal_ennreal_nndist] using edist_snd_le x y

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