Re: [isabelle] LaTeXsugar

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


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
> 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.,
>> In my humble opinion, UN i. {f i} is the better solution. (Also, what
>> about range f?)
>> Best regards,
>> Tjark

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