Re: [isabelle] LaTeXsugar

  but you find it not infrequently in
math. Here is another example (from the web, admittedly):

A sequence with terms a_n may also be referred to as "{a_n}", but contrary to
what you may have learned in other contexts, this "set" is actually an ordered
list, not an unordered collection of elements. (Your book may use some notation
other than what I'm showing here. Unfortunately, notation doesn't yet seem to
have been entirely standardized for this topic.)
Textbooks at Austrian high-schools use angle brackets: $\langle a_n \rangle$.

So, you would please that target group (still far off your target ;-)) with that or something similar, for instance $\langle\langle a_n \rangle\rangle$ in case the single brackets are occupied already.
I believe {f i}_{i : ℕ} is fairly standard to denote the *sequence* f 0,
f 1, f 2, ...; but it does not commonly denote the *set* {f i|i : ℕ}.
See, e.g.,

In my humble opinion, UN i. {f i} is the better solution. (Also, what
about range f?)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.