cylinder — Mathlib

English

In the product space ∏ n, E n, the cylinder around x of length n consists of all y that agree with x on the first n coordinates.

Русский

В произведении пространств ∏ n, E n цилиндр вокруг x длины n состоит из всех y, которые совпадают с x на первых n координатах.

LaTeX

$$$\\mathrm{cylinder}(x,n)=\\{\,y:\\; \\forall i

Lean4

/-- In a product space `Π n, E n`, the cylinder set of length `n` around `x`, denoted
`cylinder x n`, is the set of sequences `y` that coincide with `x` on the first `n` symbols, i.e.,
such that `y i = x i` for all `i < n`.
-/
def cylinder (x : ∀ n, E n) (n : ℕ) : Set (∀ n, E n) :=
  {y | ∀ i, i < n → y i = x i}

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