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:
2020_05_20-AM-08_59_37
Last ObjectModification:
2017_01_24-AM-10_54_17
Theory : lattices
Home
Index