Nuprl Definition : awf-system
awf-system{i:l}(I;A) ==
⋂T:{T:Type| ((A + (T List)) ⊆r T) ∧ (awf(A) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ (A + (T List))) ⋂ Top ⟶ I ⟶ Top
Definitions occuring in Statement :
awf: awf(T),
list: T List,
isect2: T1 ⋂ T2,
subtype_rel: A ⊆r B,
top: Top,
and: P ∧ Q,
set: {x:A| B[x]} ,
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
union: left + right,
universe: Type
Definitions occuring in definition :
isect2: T1 ⋂ T2,
isect: ⋂x:A. B[x],
set: {x:A| B[x]} ,
universe: Type,
and: P ∧ Q,
subtype_rel: A ⊆r B,
awf: awf(T),
union: left + right,
list: T List,
function: x:A ⟶ B[x],
top: Top
FDL editor aliases :
awf-system
Latex:
awf-system\{i:l\}(I;A) ==
\mcap{}T:\{T:Type| ((A + (T List)) \msubseteq{}r T) \mwedge{} (awf(A) \msubseteq{}r T)\} . ((I {}\mrightarrow{} T) {}\mrightarrow{} I {}\mrightarrow{} (A + (T List))) \mcap{} Top
{}\mrightarrow{} I
{}\mrightarrow{} Top
Date html generated:
2016_05_15-PM-07_25_20
Last ObjectModification:
2015_09_23-AM-08_14_54
Theory : general
Home
Index