Nuprl Definition : t-sqle
t-sqle(T;a;b) == ↓∃a':per-class(T;a). ∃b':per-class(T;b). (a' ≤ b')
Definitions occuring in Statement :
per-class: per-class(T;a),
exists: ∃x:A. B[x],
squash: ↓T,
sqle: s ≤ t
Definitions occuring in definition :
squash: ↓T,
exists: ∃x:A. B[x],
per-class: per-class(T;a),
sqle: s ≤ t
FDL editor aliases :
t-sqle
Latex:
t-sqle(T;a;b) == \mdownarrow{}\mexists{}a':per-class(T;a). \mexists{}b':per-class(T;b). (a' \mleq{} b')
Date html generated:
2016_05_13-PM-04_12_44
Last ObjectModification:
2015_09_22-PM-05_45_57
Theory : subtype_1
Home
Index