Theorems · Definition · combinatorics

List.Pi.cons

{ι : Type u_1} →
  [DecidableEq ι] →
    {α : ι → Sort u_2} → (i : ι) → (l : List ι) → α i → ((j : ι) → j ∈ l → α j) → (j : ι) → j ∈ i :: l → α j

Given α : ι → Sort*, a list l and a term i, as well as a term a : α i and a function f such that f j : α j for all j in l, Pi.cons a f is a function g such that g k : α k for all k in i :: l.

Defined in

Mathlib.Data.List.Pi

Cited by

9 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

DecidableEq