zip — Mathlib

English

The operation zip pairs two chains c0 and c1 of α and β into a chain of pairs in α × β via the product morphism.

Русский

Операция zip объединяет две цепи c0 и c1 над α и β в цепь пар над α × β через произведение морфизмов.

LaTeX

$$$\\text{zip}(c_0,c_1) = \\text{OrderHom}.\\text{prod}(c_0,c_1)$$$

Lean4

/-- `OmegaCompletePartialOrder.Chain.zip` pairs up the elements of two chains
that have the same index. -/
-- Not `@[simps]`: we need `@[simps!]` to see through the type synonym `Chain β = ℕ →o β`,
-- but then we'd get the `FunLike` instance for `OrderHom` instead.

def zip (c₀ : Chain α) (c₁ : Chain β) : Chain (α × β) :=
  OrderHom.prod c₀ c₁

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