## Stream: general

### Topic: notation for cardinalities

#### Eric Rodriguez (Jun 03 2021 at 20:34):

I'm planning to make a (localized?) notation for the cardinalities of sets and types, and I was thinking of using | and ‖ (kind of like what is currently used in card_embedding.lean. Does anyone have any objections to this, anything to watch out for? Should I make a notation class for either of these? Not sure whether they are used much elsewhere in Lean

#### Yakov Pechersky (Jun 03 2021 at 20:51):

We have this I think, docs#cardinal

#### Yakov Pechersky (Jun 03 2021 at 20:51):

And for finite types and sets, fintype.card and finset.card

#### Yakov Pechersky (Jun 03 2021 at 20:52):

Finally, for set cardinality where you want a regular old nat, docs#nat.card

#### Eric Wieser (Jun 03 2021 at 20:53):

Perhaps we could introduce #ᶠ for fintype.card since # is cardinal.mk?

#### Eric Rodriguez (Jun 03 2021 at 21:17):

that seems reasonable, and what about for finsets?

#### Eric Rodriguez (Jun 03 2021 at 21:21):

maybe #^s? (I can't find superscript s - does it exist?)

#### Yakov Pechersky (Jun 03 2021 at 22:22):

Why not just use projection notation for finset? Similarly, rename nat.card to set.card?

#### Eric Rodriguez (Jun 03 2021 at 22:24):

in my experience, it's been really annoying mixing up fintype and finset cards

#### Eric Rodriguez (Jun 03 2021 at 22:25):

this is why I liked the |set| and ‖type‖ idea but think the $\#^f$ seems reasonable for mathlib consistency

#### Yakov Pechersky (Jun 03 2021 at 22:41):

Can you share where they're confusing?

#### Eric Rodriguez (Jun 04 2021 at 00:10):

Most places where they have been I've made it local notation, but for example I've got a big proof in https://github.com/ericrbg/HatGames and that would be illegible without it I think, the .cards end up being sprinkled everywhere and ruining the flow

Last updated: Dec 20 2023 at 11:08 UTC