map — Mathlib

English

Given f : α ⟹ β, map sends ⟨a, g⟩ ∈ P α to ⟨a, g ∘ f⟩ ∈ P β, i.e., it acts by composing the second component with f.

Русский

Пусть f : α ⟹ β. Отображение map переводит ⟨a, g⟩ ∈ P α в ⟨a, g ∘ f⟩ ∈ P β, т.е. действует путем композирования второй компоненты с f.

LaTeX

$$$$ \\mathrm{map}(f): P(α) \\to P(β),\\quad \\mathrm{map}(f)(\\langle a, g \\rangle) = \\langle a, g \\circ f \\rangle. $$$$

Lean4

/-- Applying `P` to a morphism of `Type` -/
def map {α β : TypeVec n} (f : α ⟹ β) : P α → P β := fun ⟨a, g⟩ => ⟨a, TypeVec.comp f g⟩

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