castLastB

Mathlib.Data.PFunctor.Multivariate.M

URI: https://scilib.ai/kg/mathlib#MvPFunctor.castLastB

English

Given an equality a = a', transport the last-coordinate component through the equality.

Русский

Дано равенство a = a' переносим последнюю координату через это равенство.

LaTeX

$$$castLastB : a = a' \\to (P.last.B a) \\to (P.last.B a')$$$

Lean4

/-- Proof of type equality as a function -/
def castLastB {a a' : P.A} (h : a = a') : P.last.B a → P.last.B a' := fun b => Eq.recOn h b

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

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

Разделы

Аффилиация

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