Nuprl Definition : lg-exists
lg-exists(G;x.P[x]) == ∃n:ℕlg-size(G). P[lg-label(G;n)]
Definitions occuring in Statement :
lg-label: lg-label(g;x),
lg-size: lg-size(g),
int_seg: {i..j-},
exists: ∃x:A. B[x],
natural_number: $n
FDL editor aliases :
lg-exists
Latex:
lg-exists(G;x.P[x]) == \mexists{}n:\mBbbN{}lg-size(G). P[lg-label(G;n)]
Date html generated:
2015_07_23-AM-11_04_40
Last ObjectModification:
2012_02_25-PM-03_36_38
Home
Index