Nuprl Definition : global-order-compat
L1 || L2 == ∀i:Id. filter(λx.fst(x) = i;L1) || filter(λx.fst(x) = i;L2)
Definitions occuring in Statement :
eq_id: a = b,
Id: Id,
compat: l1 || l2,
filter: filter(P;l),
pi1: fst(t),
all: ∀x:A. B[x],
lambda: λx.A[x],
product: x:A × B[x]
FDL editor aliases :
global-order-compat
Latex:
L1 || L2 == \mforall{}i:Id. filter(\mlambda{}x.fst(x) = i;L1) || filter(\mlambda{}x.fst(x) = i;L2)
Date html generated:
2015_07_21-PM-04_38_54
Last ObjectModification:
2014_08_07-PM-01_05_04
Home
Index