map — Mathlib

English

Given a chain c and morphisms f: α →o β, the map c.map f is the chain in β obtained by composing f with c.

Русский

Дана цепь c и морфизмы f: α →o β; c.map f — цепь в β, полученная композицией f с c.

LaTeX

$$$\\text{map}: \\text{Chain}(\\alpha) \\to \\text{Chain}(\\beta)$ is defined by $c.map\,f = f \\circ c$.$$

Lean4

/-- `map` function for `Chain` -/
-- 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 map : Chain β :=
  f.comp c

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