Nuprl Definition : monotone

monotone(T;T';x,y.R[x; y];x,y.R'[x; y];f) == ∀x,y:T. (R[x; y] ⇒ R'[f x; f y])

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

Latex:
monotone(T;T';x,y.R[x; y];x,y.R'[x; y];f) == \mforall{}x,y:T. (R[x; y] {}\mRightarrow{} R'[f x; f y]) Date html generated: 2016_05_15-PM-00_03_05 Last ObjectModification: 2015_09_23-AM-06_23_58 Theory : gen_algebra_1 Home Index