## 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: May 17 2021 at 15:13 UTC