Nuprl Definition : flattice-equiv
flattice-equiv(X;x;y) ==
  ↓∃as,bs:(X + X) List List
    ((x = as ∈ Point(free-dl(X + X)))
    ∧ (y = bs ∈ Point(free-dl(X + X)))
    ∧ flattice-order(X;as;bs)
    ∧ flattice-order(X;bs;as))
Definitions occuring in Statement : 
flattice-order: flattice-order(X;as;bs)
, 
free-dl: free-dl(X)
, 
lattice-point: Point(l)
, 
list: T List
, 
exists: ∃x:A. B[x]
, 
squash: ↓T
, 
and: P ∧ Q
, 
union: left + right
, 
equal: s = t ∈ T
Definitions occuring in definition : 
squash: ↓T
, 
exists: ∃x:A. B[x]
, 
list: T List
, 
equal: s = t ∈ T
, 
lattice-point: Point(l)
, 
free-dl: free-dl(X)
, 
union: left + right
, 
and: P ∧ Q
, 
flattice-order: flattice-order(X;as;bs)
FDL editor aliases : 
flattice-equiv
Latex:
flattice-equiv(X;x;y)  ==
    \mdownarrow{}\mexists{}as,bs:(X  +  X)  List  List
        ((x  =  as)  \mwedge{}  (y  =  bs)  \mwedge{}  flattice-order(X;as;bs)  \mwedge{}  flattice-order(X;bs;as))
Date html generated:
2017_02_21-AM-09_57_48
Last ObjectModification:
2017_01_24-AM-10_54_17
Theory : lattices
Home
Index