Nuprl Definition : flattice-order
flattice-order(X;as;bs) == (∀b∈bs.(∃x∈b. (∃y∈b. y = flip-union(x) ∈ (X + X))) ∨ (∃a∈as. a ⊆ b))
Definitions occuring in Statement :
flip-union: flip-union(x),
l_contains: A ⊆ B,
l_exists: (∃x∈L. P[x]),
l_all: (∀x∈L.P[x]),
or: P ∨ Q,
union: left + right,
equal: s = t ∈ T
Definitions occuring in definition :
l_all: (∀x∈L.P[x]),
or: P ∨ Q,
equal: s = t ∈ T,
flip-union: flip-union(x),
l_exists: (∃x∈L. P[x]),
l_contains: A ⊆ B,
union: left + right
FDL editor aliases :
flattice-order
Latex:
flattice-order(X;as;bs) == (\mforall{}b\mmember{}bs.(\mexists{}x\mmember{}b. (\mexists{}y\mmember{}b. y = flip-union(x))) \mvee{} (\mexists{}a\mmember{}as. a \msubseteq{} b))
Date html generated:
2020_05_20-AM-08_59_11
Last ObjectModification:
2017_01_24-AM-10_47_07
Theory : lattices
Home
Index