Nuprl Definition : rel-monotone
rel-monotone{i:l}(T;R.F[R]) == ∀R1,R2:T ⟶ T ⟶ ℙ. (R1 => R2 ⇒ F[R1] => F[R2])
Definitions occuring in Statement :
rel_implies: R1 => R2,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
prop: ℙ,
implies: P ⇒ Q,
rel_implies: R1 => R2
FDL editor aliases :
rel-monotone
Latex:
rel-monotone\{i:l\}(T;R.F[R]) == \mforall{}R1,R2:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}. (R1 => R2 {}\mRightarrow{} F[R1] => F[R2])
Date html generated:
2016_05_14-AM-06_04_54
Last ObjectModification:
2015_09_22-PM-05_46_49
Theory : relations
Home
Index