cylinder_eq_res — Mathlib

English

cylinder x n equals the set { y | res y n = res x n }.

Русский

Цилиндр x n равен множеству { y | res y n = res x n }.

LaTeX

$$$\\mathrm{cylinder}(x,n)=\\{y\\;|\\;\\mathrm{res}(y,n)=\\mathrm{res}(x,n)\\}$$$

Lean4

/-- `cylinder x n` is equal to the set of sequences `y` with the same restriction to `n` as `x`. -/
theorem cylinder_eq_res (x : ℕ → α) (n : ℕ) : cylinder x n = {y | res y n = res x n} :=
  by
  ext y
  dsimp [cylinder]
  rw [res_eq_res]

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