Nuprl Definition : strong-subtype
strong-subtype(A;B) == (A ⊆r B) c∧ ({b:B| ∃a:A. (b = a ∈ B)} ⊆r A)
Definitions occuring in Statement :
subtype_rel: A ⊆r B,
cand: A c∧ B,
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions occuring in definition :
cand: A c∧ B,
subtype_rel: A ⊆r B,
set: {x:A| B[x]} ,
exists: ∃x:A. B[x],
equal: s = t ∈ T
FDL editor aliases :
strong-subtype
Latex:
strong-subtype(A;B) == (A \msubseteq{}r B) c\mwedge{} (\{b:B| \mexists{}a:A. (b = a)\} \msubseteq{}r A)
Date html generated:
2016_05_13-PM-04_10_51
Last ObjectModification:
2015_09_22-PM-05_45_55
Theory : subtype_1
Home
Index