zip_coe — Mathlib

English

Let c0: Chain α and c1: Chain β. For every natural number n, the nth element of the zip c0 with c1 is the pair of the nth elements, i.e. (c0.zip c1)(n) = (c0(n), c1(n)).

Русский

Пусть c0: цепь α, и c1: цепь β. Для каждого натурального числа n элемент цепи zip(c0, c1) равен паре (c0(n), c1(n)); то есть (c0.zip c1)(n) = (c0(n), c1(n)).

LaTeX

$$$$ \forall c_0 : \text{Chain } \alpha, \forall c_1 : \text{Chain } \beta, \forall n : \mathbb{N}, \ (c_0.zip c_1)\,n = (c_0\,n, c_1\,n). $$$$

Lean4

@[simp]
theorem zip_coe (c₀ : Chain α) (c₁ : Chain β) (n : ℕ) : c₀.zip c₁ n = (c₀ n, c₁ n) :=
  rfl

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