mpr — Mathlib

English

If α and β are TypeVec n with an equality h : α = β, there is a canonical arrow α ⟹ β given by transporting along h.

Русский

Если α и β — TypeVec n и есть равенство h : α = β, существует каноническая стрела α ⟹ β, полученная переносом вдоль h.

LaTeX

$$$\mathrm{mp}\{\alpha,\beta:\mathrm{TypeVec} n\}(h):\alpha \Rightarrow \beta$ where $(\mathrm{mp}(h))(i)=\mathrm{Eq.mp}(\mathrm{congr\_fun} h i)$$$

Lean4

/-- turn an equality into an arrow, with reverse direction -/
def mpr {α β : TypeVec n} (h : α = β) : β ⟹ α
  | _ => Eq.mpr (congr_fun h _)

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