mp

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.Arrow.mp

English

Applying splitFun to f and g and then taking lastFun recovers g: lastFun (splitFun f g) = g.

Русский

Применение splitFun к f и g, а затем взятие последней координаты восстанавливает g.

LaTeX

$$$\mathrm{lastFun}(\mathrm{splitFun} f g) = g$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru