This is an old revision of the document!
Reversed relation
Definition
$ R $ |
$ \forall_R c\ \exists a,b\ (c=\langle a,b\rangle) $ |
$ \langle x,y \rangle \in R^\smile $ |
---|
$ \langle y,x \rangle \in R $ |
---|
Ramifications
Reference
Mizar files: RELAT_1
Context
Set constructor