Nuprl Definition : seq-count

#{i<j|f i eq x} ==  𝔹size(j;(eq x) o f)


Definitions occuring in Statement :  bool-size: 𝔹size(k;f),  compose: f o g,  apply: f a
Definitions occuring in definition :  bool-size: 𝔹size(k;f),  compose: f o g,  apply: f a
FDL editor aliases :  seq-count
Latex:
\#\{i<j|f  i  eq  x\}  ==    \mBbbB{}size(j;(eq  x)  o  f)


Date html generated: 2016_05_15-PM-04_43_45
Last ObjectModification: 2015_09_23-AM-07_49_55

Theory : general


Home Index