fromTypes_succ_equiv — Mathlib

English

FromTypes p τ is equivalent to vecHead p → FromTypes (vecTail p) τ.

Русский

FromTypes p τ эквивалентно vecHead p → FromTypes (vecTail p) τ.

LaTeX

$$$FromTypes p\tau \simeq (\mathrm{vecHead} \ p \to FromTypes(\mathrm{vecTail} p) \tau)$$$

Lean4

/-- The definitional equality between `p`-ary heterogeneous functions into `τ`
  and function from `vecHead p` to `(vecTail p)`-ary heterogeneous functions into `τ`. -/
@[simps!]
def fromTypes_succ_equiv {n} (p : Fin (n + 1) → Type u) (τ : Type u) :
    FromTypes p τ ≃ (vecHead p → FromTypes (vecTail p) τ) :=
  Equiv.refl _

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