Email Gateway (Aug 19 2022 at 09:45): Email Gateway (Aug 19 2022 at 09:45):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Sugarers,
how about adding the following to LaTeXsugar.thy?
syntax (latex output)
"_CollectIndex" ::
"pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_\<^esub>)")
translations
"_CollectIndex p i" <= "{p | i. CONST True}"
term "{f i | i. True}"
cheers
chris
Email Gateway (Aug 19 2022 at 09:45):From: Tobias Nipkow <nipkow@in.tum.de>
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 sometimes write UN i. {f i} in such cases. Of
course, it gives you a different term, but mostly it behaves the same.
Tobias
Email Gateway (Aug 19 2022 at 09:46):From: Christian Sternagel <c.sternagel@gmail.com>
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, and since all
natural numbers are ge 0, I thought, just drop it. Alternatively, we
could do the following specifically for nats:
syntax (latex output)
"_CollectIndex_nat" ::
"pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_\<ge>0\<^esub>)")
translations
"_CollectIndex_nat p i" <= "{p | (i::nat). CONST True}"
or
syntax (latex output)
"_CollectIndex_nat" ::
"pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_∈ℕ\<^esub>)")
cheers
chris
Tobias
Am 30/01/2013 04:26, schrieb Christian Sternagel:
Dear Sugarers,
how about adding the following to LaTeXsugar.thy?
syntax (latex output)
"_CollectIndex" ::
"pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_\<^esub>)")translations
"_CollectIndex p i" <= "{p | i. CONST True}"term "{f i | i. True}"
cheers
chris
Email Gateway (Aug 19 2022 at 09:49):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
and since all natural
numbers are ge 0, I thought, just drop it. Alternatively, we could do the
following specifically for nats:syntax (latex output)
"_CollectIndex_nat" ::
"pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_\<ge>0\<^esub>)")translations
"_CollectIndex_nat p i" <= "{p | (i::nat). CONST True}"or
syntax (latex output)
"_CollectIndex_nat" ::
"pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_∈ℕ\<^esub>)")cheers
chris
Tobias
Am 30/01/2013 04:26, schrieb Christian Sternagel:
Dear Sugarers,
how about adding the following to LaTeXsugar.thy?
syntax (latex output)
"_CollectIndex" ::
"pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_\<^esub>)")translations
"_CollectIndex p i" <= "{p | i. CONST True}"term "{f i | i. True}"
cheers
chris
Email Gateway (Aug 19 2022 at 09:50):From: Tjark Weber <webertj@in.tum.de>
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
Email Gateway (Aug 19 2022 at 09:50):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 09:50):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 09:50):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 19 2022 at 09:50):From: Walther Neuper <wneuper@ist.tugraz.at>
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., http://en.wikipedia.org/wiki/Sequence#IndexingIn my humble opinion, UN i. {f i} is the better solution. (Also, what
about range f?)
Last updated: Nov 21 2024 at 12:39 UTC