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:
2017_02_21-AM-09_52_49
Last ObjectModification:
2017_01_22-PM-07_05_38
Theory : lattices
Home
Index