free_map_coe — Mathlib

English

For α, β and f: α → β, the induced map on the free objects agrees with the rename map on polynomials.

Русский

Пусть α, β и f: α → β. Индукциированное отображение на свободных объектах совпадает с отображением переименования на многочленах.

LaTeX

$$$\text{free.map } f = \text{rename } f$ on carriers$$

Lean4

theorem free_map_coe {α β : Type u} {f : α → β} : ⇑(free.map f) = ⇑(rename f) :=
  rfl

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