|
Post Made Community Wiki by S. Carnahan♦
|
||||
|
|
||||
|
2 | corrected link code | ||
|
This would fit as a response to Harald Hanche-Olsen's remark, but I have not enough points for this. Anyway, Mizar mathematial library chose exactly this notation; actually, it is introduced in the article on basic relations RELAT_1.MIZ, Def. 12, so it fits any relation and any set. In a Mizar article you have just ASCII, so no subscripts, but you can always avoid ambiguities like f|X versus X|f by typing the two objects appearing in the notation as Relation and set respectively. I find interesting that what is expressible on paper by varying font size is emulated by typing in a proof checker. |
||||
|
|
1 |
|
||
|
This would fit as a response to Harald Hanche-Olsen's remark, but I have not enough points for this. Anyway, Mizar mathematial library chose exactly this notation; actually, it is introduced in the article on basic relations RELAT_1.MIZ, Def. 12, so it fits any relation and any set. In a Mizar article you have just ASCII, so no subscripts, but you can always avoid ambiguities like f|X versus X|f by typing the two objects appearing in the notation as Relation and set respectively. I find interesting that what is expressible on paper by varying font size is emulated by typing in a proof checker. |
||||
