Nuprl Definition : andrew
andrew{i:l}(T) == {c:Type| (c ⊆r T) ∧ (⋂X:c. X)}
Definitions occuring in Statement :
subtype_rel: A ⊆r B,
and: P ∧ Q,
set: {x:A| B[x]} ,
isect: ⋂x:A. B[x],
universe: Type
Definitions occuring in definition :
set: {x:A| B[x]} ,
universe: Type,
and: P ∧ Q,
subtype_rel: A ⊆r B,
isect: ⋂x:A. B[x]
FDL editor aliases :
andrew
Latex:
andrew\{i:l\}(T) == \{c:Type| (c \msubseteq{}r T) \mwedge{} (\mcap{}X:c. X)\}
Date html generated:
2016_05_15-PM-07_55_01
Last ObjectModification:
2015_09_23-AM-08_19_56
Theory : general
Home
Index