Nuprl Definition : mono
mono(T) == ∀a:T. ∀b:Base. (is-above(T;a;b) ⇒ (a = b ∈ T))
Definitions occuring in Statement :
is-above: is-above(T;a;z),
all: ∀x:A. B[x],
implies: P ⇒ Q,
base: Base,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
base: Base,
implies: P ⇒ Q,
is-above: is-above(T;a;z),
equal: s = t ∈ T
FDL editor aliases :
mono
Latex:
mono(T) == \mforall{}a:T. \mforall{}b:Base. (is-above(T;a;b) {}\mRightarrow{} (a = b))
Date html generated:
2016_05_13-PM-04_13_20
Last ObjectModification:
2015_09_22-PM-05_45_59
Theory : subtype_1
Home
Index