English
y lies in the cylinder around x of length n iff the distance is at most (1/2)^n.
Русский
y принадлежит цилиндру вокруг x длины n тогда и только тогда, когда расстояние не больше чем (1/2)^n.
LaTeX
$$$$ y \in \mathrm{cylinder}(x,n) \iff \operatorname{dist}(y,x) \le (1/2)^n $$$$
Lean4
theorem mem_cylinder_iff_dist_le {x y : ∀ n, E n} {n : ℕ} : y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n :=
by
rcases eq_or_ne y x with (rfl | hne)
· simp [PiNat.dist_self]
suffices (∀ i : ℕ, i < n → y i = x i) ↔ n ≤ firstDiff y x by simpa [dist_eq_of_ne hne]
constructor
· intro hy
by_contra! H
exact apply_firstDiff_ne hne (hy _ H)
· intro h i hi
exact apply_eq_of_lt_firstDiff (hi.trans_le h)