dist_le_dist_pi_of_dist_lt — Mathlib

English

If dist(x,y) < (1/2)^{encode i}, then dist(x_i,y_i) ≤ dist(x,y).

Русский

Если dist(x,y) < (1/2)^{encode i}, то dist(x_i,y_i) ≤ dist(x,y).

LaTeX

$$$$\\text{If } dist(x,y) < (\\\\tfrac12)^{\\\\encode i}, \\text{ then } dist(x_i,y_i) \\le dist(x,y).$$$$

Lean4

theorem dist_le_dist_pi_of_dist_lt {x y : ∀ i, F i} {i : ι} (h : dist x y < (1 / 2) ^ encode i) :
    dist (x i) (y i) ≤ dist x y := by simpa only [not_le.2 h, false_or] using min_le_iff.1 (min_dist_le_dist_pi x y i)

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