# Re: [isabelle] LaTeXsugar

```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
```
Tjark almost convinced me and I will probably switch to UN i. {f i} in my development. The only reason why I still consider \{f i\}_i nice, is its brevity (but if it does not convey the intended meaning, there is no point using it).
```
```
Initially, I got the idea for \{f i\}_{i : I} (and derived \{f i\}_i) from the notation that is used for indexed families, see e.g.
```
http://en.wikipedia.org/wiki/Indexed_family

```
But then, I was not aware that \{f i\}_{i : I} has a different meaning from \{f i | i : I\} (and in fact I'm pretty sure that I saw these notations used interchangeably, but can't put my finger on where).
```
cheers

chris

```

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