Reversed relation
Set
| context | $ R\in\text{Rel}(X,Y) $ |
| definiendum | $ \langle x,y \rangle \in R^\smile $ |
| postulate | $ \langle y,x \rangle \in R $ |
Ramifications
Reference
Mizar files: RELAT_1
Parents
Context
| context | $ R\in\text{Rel}(X,Y) $ |
| definiendum | $ \langle x,y \rangle \in R^\smile $ |
| postulate | $ \langle y,x \rangle \in R $ |
Mizar files: RELAT_1
