Nuprl Definition : lexico
lexico(T; a,b.lt[a; b]) ==
λas,bs. (||as|| < ||bs|| ∨ ((||as|| = ||bs|| ∈ ℤ) ∧ (∃i:ℕ||as||. (lt[as[i]; bs[i]] ∧ (∀j:ℕi. (as[j] = bs[j] ∈ T))))))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
less_than: a < b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
lambda: λx.A[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
or: P ∨ Q,
less_than: a < b,
int: ℤ,
exists: ∃x:A. B[x],
length: ||as||,
and: P ∧ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
equal: s = t ∈ T,
select: L[n]
Latex:
lexico(T; a,b.lt[a; b]) ==
\mlambda{}as,bs. (||as|| < ||bs||
\mvee{} ((||as|| = ||bs||) \mwedge{} (\mexists{}i:\mBbbN{}||as||. (lt[as[i]; bs[i]] \mwedge{} (\mforall{}j:\mBbbN{}i. (as[j] = bs[j]))))))
Date html generated:
2016_05_15-PM-06_35_34
Last ObjectModification:
2015_09_23-AM-08_04_19
Theory : general
Home
Index