Nuprl Definition : RankEx1
RankEx1(T) == {p:RankEx1co(T)| (RankEx1co_size(p))↓}
Definitions occuring in Statement :
RankEx1co_size: RankEx1co_size(p),
RankEx1co: RankEx1co(T),
has-value: (a)↓,
set: {x:A| B[x]}
FDL editor aliases :
RankEx1
Latex:
RankEx1(T) == \{p:RankEx1co(T)| (RankEx1co\_size(p))\mdownarrow{}\}
Date html generated:
2016_05_16-AM-08_56_13
Last ObjectModification:
2014_05_06-PM-02_34_00
Theory : C-semantics
Home
Index