mem_cylinder_iff_dist_le — Mathlib

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)

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