Theorems · Definition

Function.fromTypes_succ_equiv

{n : ℕ} →
  (p : Fin (n + 1) → Type u) →
    (τ : Type u) → Function.FromTypes p τ ≃ (Matrix.vecHead p → Function.FromTypes (Matrix.vecTail p) τ)

The definitional equality between p-ary heterogeneous functions into τ and function from vecHead p to (vecTail p)-ary heterogeneous functions into τ.

Defined in: Mathlib.Logic.Function.FromTypes
Cited by: 2 results in Mathlib
Foundations: Depth 28 from the axioms · uses propext

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Equivstatement · cited by 8,337
Equiv.reflproof · cited by 274
Matrix.vecTailstatement · cited by 39
Matrix.vecHeadstatement · cited by 34
Function.FromTypesstatement and proof · cited by 29

Cited by3

Results whose statement or proof uses this declaration.

Function.fromTypes_cons_equivproof · cited by 2
Function.fromTypes_succ_equiv_applystatement and proof · cited by 0
Function.fromTypes_succ_equiv_symm_applystatement and proof · cited by 0