Nuprl Definition : dma-lift-compose
dma-lift-compose(I;J;eqi;eqj;f;g) == free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) o g
Definitions occuring in Statement :
free-dma-lift: free-dma-lift(T;eq;dm;eq2;f),
free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq),
free-dml-deq: free-dml-deq(T;eq),
compose: f o g
Definitions occuring in definition :
compose: f o g,
free-dma-lift: free-dma-lift(T;eq;dm;eq2;f),
free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq),
free-dml-deq: free-dml-deq(T;eq)
FDL editor aliases :
dma-lift-compose
Latex:
dma-lift-compose(I;J;eqi;eqj;f;g) ==
free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) o g
Date html generated:
2020_05_20-AM-08_57_25
Last ObjectModification:
2015_10_12-PM-09_50_23
Theory : lattices
Home
Index