Nuprl Definition : rel-preserving
λx.f[x]:T2->T1 takes R2 into R1*) == ∀x,y:T2. ((x R2 y) ⇒ (f[x] (R1^*) f[y]))
Definitions occuring in Statement :
rel_star: R^*,
infix_ap: x f y,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
infix_ap: x f y,
rel_star: R^*
FDL editor aliases :
rel-preserving
Latex:
\mlambda{}x.f[x]:T2->T1 takes R2 into R1*) == \mforall{}x,y:T2. ((x R2 y) {}\mRightarrow{} (f[x] rel\_star(T1; R1) f[y]))
Date html generated:
2016_05_15-PM-05_40_14
Last ObjectModification:
2015_09_23-AM-07_58_06
Theory : general
Home
Index