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: P ⇒ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
st-atoms-distinct
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:
2015_07_17-AM-08_56_42
Last ObjectModification:
2013_03_25-PM-01_53_22
Home
Index