MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

Post Made Community Wiki by S. Carnahan

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.