Nuprl Definition : is_ufm
IsUFM(g) == ∀b:|g|. ((¬(g-unit(b)))
⇒ (≡~)∃!as:Atom{g} List. (b = (Π as) ∈ |g|))
Definitions occuring in Statement :
permr_massoc_rel: ≡~
,
exists_uni_upto: exists_uni_upto,
matom_ty: Atom{g}
,
munit: g-unit(u)
,
mon_reduce: mon_reduce,
list: T List
,
all: ∀x:A. B[x]
,
not: ¬A
,
implies: P
⇒ Q
,
equal: s = t ∈ T
,
grp_car: |g|
Definitions occuring in definition :
all: ∀x:A. B[x]
,
implies: P
⇒ Q
,
not: ¬A
,
munit: g-unit(u)
,
exists_uni_upto: exists_uni_upto,
list: T List
,
matom_ty: Atom{g}
,
permr_massoc_rel: ≡~
,
equal: s = t ∈ T
,
grp_car: |g|
,
mon_reduce: mon_reduce
Latex:
IsUFM(g) == \mforall{}b:|g|. ((\mneg{}(g-unit(b))) {}\mRightarrow{} (\mequiv{}\msim{})\mexists{}!as:Atom\{g\} List. (b = (\mPi{} as)))
Date html generated:
2016_05_16-AM-07_45_19
Last ObjectModification:
2015_09_23-AM-09_51_58
Theory : factor_1
Home
Index