Nuprl Definition : rels_iso
(basic):: RelsIso(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],
iff: P ⇐⇒ Q,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a
Latex:
(basic):: RelsIso(T;T';x,y.R[x; y];x,y.R'[x; y];f) == \mforall{}x,y:T. (R[x; y] \mLeftarrow{}{}\mRightarrow{} R'[f x; f y])
Date html generated:
2016_05_15-PM-00_03_08
Last ObjectModification:
2015_09_23-AM-06_23_59
Theory : gen_algebra_1
Home
Index