apply_eq_of_dist_lt — Mathlib

English

If dist(x,y) < (1/2)^n then x_i = y_i for all i ≤ n.

Русский

Если dist(x,y) < (1/2)^n, то для всех i ≤ n выполняется x_i = y_i.

LaTeX

$$$$ \operatorname{dist}(x,y) < (1/2)^n \Rightarrow \forall i\le n, \; x(i)=y(i) $$$$

Lean4

theorem apply_eq_of_dist_lt {x y : ∀ n, E n} {n : ℕ} (h : dist x y < (1 / 2) ^ n) {i : ℕ} (hi : i ≤ n) : x i = y i :=
  by
  rcases eq_or_ne x y with (rfl | hne)
  · rfl
  have : n < firstDiff x y := by simpa [dist_eq_of_ne hne, inv_lt_inv₀, pow_lt_pow_iff_right₀, one_lt_two] using h
  exact apply_eq_of_lt_firstDiff (hi.trans_lt this)

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