Nuprl Definition : order-preserving
order-preserving(A;B;a1,a2.R1[a1; a2];b1,b2.R2[b1; b2];f) == ∀a1,a2:A. (R1[a1; a2] ⇒ R2[f a1; f a2])
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a
FDL editor aliases :
order-preserving
Latex:
order-preserving(A;B;a1,a2.R1[a1; a2];b1,b2.R2[b1; b2];f) ==
\mforall{}a1,a2:A. (R1[a1; a2] {}\mRightarrow{} R2[f a1; f a2])
Date html generated:
2016_05_15-PM-03_28_29
Last ObjectModification:
2015_09_23-AM-07_43_33
Theory : general
Home
Index