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: List exists: x:A. B[x] squash: T and: P ∧ Q union: left right equal: t ∈ T
Definitions occuring in definition :  squash: T exists: x:A. B[x] list: List equal: 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