x,y:T. R(x;y) 
R(y;x) x = yT:Type, R:(T
TProp). AntiSym(T;x,y.R(x,y)) 
Prop| Who Cites anti sym? | |
| anti_sym | Def AntiSym(T;x,y.R(x;y)) == x,y:T. R(x;y) R(y;x) x = y |
| Thm* T:Type, R:(TTProp). AntiSym(T;x,y.R(x,y)) Prop |
| Syntax: | AntiSym(T;x,y.R(x;y)) | has structure: | anti_sym(T; x,y.R(x;y)) |
About:
 |  |  |  |  |  |  |  |