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; y])



Definitions occuring in Statement :  all: x:A. B[x] iff: ⇐⇒ Q apply: a
Definitions occuring in definition :  all: x:A. B[x] iff: ⇐⇒ Q apply: 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