mathlib3 documentation

data.qpf.multivariate.constructions.sigma

Dependent product and sum of QPFs are QPFs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def mvqpf.sigma {n : } {A : Type u} (F : A typevec n Type u) (v : typevec n) :

Dependent sum of of an n-ary functor. The sum can range over data types like or over Type.{u-1}

Equations
Instances for mvqpf.sigma
def mvqpf.pi {n : } {A : Type u} (F : A typevec n Type u) (v : typevec n) :

Dependent product of of an n-ary functor. The sum can range over data types like or over Type.{u-1}

Equations
Instances for mvqpf.pi
@[protected, instance]
def mvqpf.sigma.inhabited {n : } {A : Type u} (F : A typevec n Type u) {α : typevec n} [inhabited A] [inhabited (F inhabited.default α)] :
Equations
@[protected, instance]
def mvqpf.pi.inhabited {n : } {A : Type u} (F : A typevec n Type u) {α : typevec n} [Π (a : A), inhabited (F a α)] :
Equations
@[protected, instance]
def mvqpf.sigma.mvfunctor {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] :
Equations
@[protected]
def mvqpf.sigma.P {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

polynomial functor representation of a dependent sum

Equations
@[protected]
def mvqpf.sigma.abs {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :

abstraction function for dependent sums

Equations
@[protected]
def mvqpf.sigma.repr {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :

representation function for dependent sums

Equations
@[protected, instance]
def mvqpf.sigma.mvqpf {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :
Equations
@[protected, instance]
def mvqpf.pi.mvfunctor {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] :
Equations
@[protected]
def mvqpf.pi.P {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

polynomial functor representation of a dependent product

Equations
@[protected]
def mvqpf.pi.abs {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :

abstraction function for dependent products

Equations
@[protected]
def mvqpf.pi.repr {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :

representation function for dependent products

Equations
@[protected, instance]
def mvqpf.pi.mvqpf {n : } {A : Type u} (F : A typevec n Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :
Equations