dropFun_RelLast'

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.dropFun_RelLast'

English

Dropping the functor from RelLast'(α, R) yields the repeatEq α.

Русский

dropFun от RelLast'(α, R) даёт repeatEq α.

LaTeX

$$\operatorname{dropFun}(\operatorname{RelLast}'(\alpha, R)) = \operatorname{repeatEq}(\alpha)$$

Lean4

@[simp]
theorem dropFun_RelLast' {α : TypeVec n} {β} (R : β → β → Prop) : dropFun (RelLast' α R) = repeatEq α :=
  rfl

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

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

Разделы

Аффилиация

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