Zulip Chat Archive

Stream: Is there code for X?

Topic: Absolute value for cardinality


Bjørn Kjos-Hanssen (Oct 21 2020 at 21:38):

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

Heather Macbeth (Oct 21 2020 at 21:40):

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

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!

Kevin Buzzard (Oct 21 2020 at 21:41):

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

Kevin Buzzard (Oct 21 2020 at 21:41):

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

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

Bjørn Kjos-Hanssen (Oct 21 2020 at 21:43):

Thanks, that was easy!

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

Kevin Buzzard (Oct 21 2020 at 21:44):

It might work fine though!

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

Mario Carneiro (Oct 21 2020 at 23:03):

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

Mario Carneiro (Oct 21 2020 at 23:04):

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


Last updated: Dec 20 2023 at 11:08 UTC