min_dist_le_dist_pi — Mathlib

English

For each i, min((1/2)^{encode i}, dist(x_i,y_i)) ≤ dist(x,y).

Русский

Для каждого i выполняется неравенство: min((1/2)^{encode i}, dist(x_i,y_i)) ≤ dist(x,y).

LaTeX

$$$$\\\\min((\\\\tfrac12)^{\\\\encode i},\\\\ dist(x_i,y_i)) \\\\leq \\\\ dist(x,y).$$$$

Lean4

theorem min_dist_le_dist_pi (x y : ∀ i, F i) (i : ι) : min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i)) ≤ dist x y :=
  (dist_summable x y).le_tsum i fun j _ => le_min (by simp) dist_nonneg

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