atoms-distinct(tab) ==
i,j:
||tab|| . ((st-atom(tab;i) = st-atom(tab;j)) 
(i = j))
Definitions :
all: x:A. B[x],
int_seg: {i..j
},
natural_number: $n,
st-length: ||tab|| ,
implies: P Q,
atom: Atom$n,
st-atom: st-atom(tab;n),
equal: s = t,
int: 
FDL editor aliases :
st-atoms-distinct
atoms-distinct(tab) == \mforall{}i,j:\mBbbN{}||tab|| . ((st-atom(tab;i) = st-atom(tab;j)) {}\mRightarrow{} (i = j))
Date html generated:
2010_08_27-AM-09_33_55
Last ObjectModification:
2009_12_16-AM-01_14_19
Home
Index