*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] LaTeXsugar*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 31 Jan 2013 08:41:15 +0100*In-reply-to*: <510A09B7.6090108@gmail.com>*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>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130107 Thunderbird/17.0.2

I agree that this convention is unfortunate, 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.) Tobias Am 31/01/2013 07:05, schrieb Christian Sternagel: > Another 2 of my cents (euro): > > I worked quite a lot with sequences but never (consciously) encountered or used > the notation from > > http://en.wikipedia.org/wiki/Sequence#Indexing > > And in fact it seems quite misleading to me to use curly brackets (that have a > strong association with sets) when dealing with ordered sequences. > > cheers > > chris > > > On 01/31/2013 07:17 AM, Tjark Weber wrote: >> On Wed, 2013-01-30 at 22:16 +0100, Tobias Nipkow wrote: >>> Am 30/01/2013 14:53, schrieb Christian Sternagel: >>>> On 01/30/2013 04:03 PM, Tobias Nipkow wrote: >>>>> I don't like the {f i|i. True} syntax either but your {f i}_i is a bit >>>>> non-standard, too, isn't it? >>>> I don't know ;). I think {f i}_{i : ℕ} is fairly standard, >>> >>> If you can convince me of that, I'll probably add your original syntax (unless >>> other problems crop up). I am just unsure myself, although it looks plausible. >> >> 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?) >> >> Best regards, >> Tjark >> >> >> >

**Follow-Ups**:**Re: [isabelle] LaTeXsugar***From:*Walther Neuper

**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

- Previous by Date: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: Re: [isabelle] Evaluation of List.coset
- Previous by Thread: Re: [isabelle] LaTeXsugar
- Next by Thread: Re: [isabelle] LaTeXsugar
- 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