*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] LaTeXsugar*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Thu, 31 Jan 2013 09:09:23 +0100*In-reply-to*: <510A201B.9030104@in.tum.de>*References*: <510892D9.1010408@gmail.com> <5108C5B9.1020305@in.tum.de> <510925D8.4020404@gmail.com> <51098D9E.3050000@in.tum.de> <1359584222.23351.26.camel@weber> <510A09B7.6090108@gmail.com> <510A201B.9030104@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:15.0) Gecko/20120912 Thunderbird/15.0.1

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.)

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., http://en.wikipedia.org/wiki/Sequence#Indexing In my humble opinion, UN i. {f i} is the better solution. (Also, what about range f?)

**References**:**[isabelle] LaTeXsugar***From:*Christian Sternagel

**Re: [isabelle] LaTeXsugar***From:*Tobias Nipkow

**Re: [isabelle] LaTeXsugar***From:*Christian Sternagel

**Re: [isabelle] LaTeXsugar***From:*Tobias Nipkow

**Re: [isabelle] LaTeXsugar***From:*Tjark Weber

**Re: [isabelle] LaTeXsugar***From:*Christian Sternagel

**Re: [isabelle] LaTeXsugar***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Evaluation of List.coset
- Next by Date: [isabelle] Surprises with transfer method
- Previous by Thread: Re: [isabelle] LaTeXsugar
- Next by Thread: [isabelle] excluding theories from html pages
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list