Nuprl Definition : st-atoms-distinct

atoms-distinct(tab) ==  ∀i,j:ℕ||tab|| .  ((st-atom(tab;i) st-atom(tab;j) ∈ Atom1)  (i j ∈ ℤ))



Definitions occuring in Statement :  st-atom: st-atom(tab;n) st-length: ||tab||  int_seg: {i..j-} atom: Atom$n all: x:A. B[x] implies:  Q natural_number: $n int: equal: t ∈ T
FDL editor aliases :  st-atoms-distinct st-atoms-distinct

Latex:
atoms-distinct(tab)  ==    \mforall{}i,j:\mBbbN{}||tab||  .    ((st-atom(tab;i)  =  st-atom(tab;j))  {}\mRightarrow{}  (i  =  j))



Date html generated: 2016_05_16-AM-10_02_09
Last ObjectModification: 2013_03_25-PM-01_53_22

Theory : new!event-ordering


Home Index