English
Let ι be a finite index set and x, y, x', y' be functions ι → ℝ such that for every i ∈ ι, x(i), y(i) ∈ Icc(x'(i), y'(i)). Then the product-distance dist x y is bounded by dist x' y'.
Русский
Пусть ι конечен, и функции x, y, x', y': ι → ℝ удовлетворяют, что для каждого i ∈ ι выполняется x(i), y(i) ∈ Icc(x'(i), y'(i)). Тогда расстояние между векторами x и y в произведении не превосходит расстояния между x' и y'.
LaTeX
$$$\\forall {\\iota} [Fintype \\iota] \\ {x y x' y' : \\iota \\to \\mathbb{R}},\\ (x \\in Icc(x',y') \\Rightarrow y \\in Icc(x',y')) \\Rightarrow \\operatorname{dist}_\\text{prod}(x,y) \\le \\operatorname{dist}_\\text{prod}(x',y')$$$
Lean4
theorem dist_le_of_mem_pi_Icc (hx : x ∈ Icc x' y') (hy : y ∈ Icc x' y') : dist x y ≤ dist x' y' :=
by
refine (dist_pi_le_iff dist_nonneg).2 fun b => (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b) <;>
refine Icc_subset_uIcc ?_
exacts [⟨hx.1 _, hx.2 _⟩, ⟨hy.1 _, hy.2 _⟩]
