Absolute value for cardinality

Stream: Is there code for X?

[Bjørn Kjos-Hanssen]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Heather Macbeth]

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]

Thanks, that was easy!

[Kevin Buzzard]

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

It might work fine though!

[Bjørn Kjos-Hanssen]

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

[Mario Carneiro]

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

[Mario Carneiro]

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