Nuprl Definition : lg-all
∀x∈G.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-},
all: ∀x:A. B[x],
natural_number: $n
FDL editor aliases :
lg-all
Latex:
\mforall{}x\mmember{}G.P[x] == \mforall{}n:\mBbbN{}lg-size(G). P[lg-label(G;n)]
Date html generated:
2015_07_23-AM-11_04_33
Last ObjectModification:
2012_02_25-PM-03_36_27
Home
Index