Nuprl Definition : dlattice-order
as 
⇒ bs ==  (∀b∈bs.(∃a∈as. a ⊆ b))
Definitions occuring in Statement : 
l_contains: A ⊆ B
, 
l_exists: (∃x∈L. P[x])
, 
l_all: (∀x∈L.P[x])
Definitions occuring in definition : 
l_all: (∀x∈L.P[x])
, 
l_exists: (∃x∈L. P[x])
, 
l_contains: A ⊆ B
FDL editor aliases : 
dlattice-order
Latex:
as  {}\mRightarrow{}  bs  ==    (\mforall{}b\mmember{}bs.(\mexists{}a\mmember{}as.  a  \msubseteq{}  b))
Date html generated:
2020_05_20-AM-08_26_25
Last ObjectModification:
2017_01_22-PM-07_05_38
Theory : lattices
Home
Index