Nuprl Definition : order-type-less
WFO x has a strictly smaller order type than WFO y when
there is an order-preserving map from x to y whose range
is bounded by some member of y.⋅
order-type-less() ==
λx,y. let A,R,wf1 = x in
let B,S,wf2 = y in
∃f:A ⟶ B. ∃b:B. (order-preserving(A;B;a1,a2.a1 R a2;b1,b2.b1 S b2;f) ∧ (∀a:A. ((f a) S b)))
Definitions occuring in Statement :
order-preserving: order-preserving(A;B;a1,a2.R1[a1; a2];b1,b2.R2[b1; b2];f),
spreadn: spread3,
infix_ap: x f y,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x]
Definitions occuring in definition :
lambda: λx.A[x],
spreadn: spread3,
function: x:A ⟶ B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
order-preserving: order-preserving(A;B;a1,a2.R1[a1; a2];b1,b2.R2[b1; b2];f),
all: ∀x:A. B[x],
infix_ap: x f y,
apply: f a
FDL editor aliases :
order-type-less
Latex:
order-type-less() ==
\mlambda{}x,y. let A,R,wf1 = x in
let B,S,wf2 = y in
\mexists{}f:A {}\mrightarrow{} B. \mexists{}b:B. (order-preserving(A;B;a1,a2.a1 R a2;b1,b2.b1 S b2;f) \mwedge{} (\mforall{}a:A. ((f a) S b)))
Date html generated:
2016_07_08-PM-05_02_12
Last ObjectModification:
2015_09_23-AM-07_46_57
Theory : general
Home
Index