mem_cylinder_iff — Mathlib

English

A sequence y lies in cylinder x n if and only if for every i < n, y i = x i.

Русский

Последовательность y принадлежит цилиндру вокруг x длины n тогда и только тогда, когда для каждого i < n выполняется y i = x i.

LaTeX

$$$y\\in\\mathrm{cylinder}(x,n)\\iff \\forall i

Lean4

@[simp]
theorem mem_cylinder_iff {x y : ∀ n, E n} {n : ℕ} : y ∈ cylinder x n ↔ ∀ i < n, y i = x i :=
  Iff.rfl

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