Zulip Chat Archive

Stream: Is there code for X?

Topic: Absolute value for cardinality


view this post on Zulip Bjørn Kjos-Hanssen (Oct 21 2020 at 21:38):

Is there a way we can define |X| to mean X.card?

view this post on Zulip Heather Macbeth (Oct 21 2020 at 21:40):

I think you can do something like local notation |X| := finset.card X(unchecked).

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 21:41):

The easiest way would be to dig up some unicode vertical lines which haven't been used before in mathlib and then add this as notation. The issue with | and \| is that they're already used to mean other things (several other things in the former case). You could try it though!

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 21:41):

Heather has also uncovered a Zulip puzzle for us :-)

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 21:41):

local notation `|`X`|` := finset.card X?

view this post on Zulip Heather Macbeth (Oct 21 2020 at 21:42):

Compare, for example, the line in #tutorials defining local notation for the absolute value
https://github.com/leanprover-community/tutorials/blob/6c0866ea177e5336e4e0592aac744f966d784117/src/exercises/00_first_proofs.lean#L260

view this post on Zulip Bjørn Kjos-Hanssen (Oct 21 2020 at 21:43):

Thanks, that was easy!

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 21:44):

...until it starts giving you random errors because your set { |X| } is mis-parsed by the parser as being some set such that...syntax error...

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 21:44):

It might work fine though!

view this post on Zulip Bjørn Kjos-Hanssen (Oct 21 2020 at 21:45):

Yes, I don't need to also use set builder notation for what I'm working on

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:03):

Hopefully you also don't need definitions with the equation compiler or inductive types

view this post on Zulip Mario Carneiro (Oct 21 2020 at 23:04):

then again, I think a mathematician can probably go without those fairly well


Last updated: May 17 2021 at 15:13 UTC