wMap — Mathlib

English

W-types are functorial: given a map g between the labels, there is a corresponding map wMap g : W α → W β transporting trees by applying g to each leaf label.

Русский

W-типы являются функторными: задано отображение g между обозначениями, существует отображение wMap g: W α → W β, переносом дерева путем применения g к каждому листу.

LaTeX

$$$ wMap\, g\, x = g <$$> x $$$

Lean4

/-- W-types are functorial -/
def wMap {α β : TypeVec n} (g : α ⟹ β) : P.W α → P.W β := fun x => g <$$> x

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