Nuprl Definition : global-order-iseg
L1 ≤ L2, locally == ∀i:Id. filter(λx.fst(x) = i;L1) ≤ filter(λx.fst(x) = i;L2)
Definitions occuring in Statement :
eq_id: a = b,
Id: Id,
iseg: 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-iseg
Latex:
L1 \mleq{} L2, locally == \mforall{}i:Id. filter(\mlambda{}x.fst(x) = i;L1) \mleq{} filter(\mlambda{}x.fst(x) = i;L2)
Date html generated:
2015_07_21-PM-04_36_53
Last ObjectModification:
2014_08_07-PM-01_06_29
Home
Index