Zero in 3.6.14 cardinality exercises

Stream: Analysis I

[Dan Abramov]

I'm finding cardinality exercises (3.6.14) fun to work out except for one detail — how empty sets are represented.

Concretely, I often end up having .card = 0 because it's actually empty (like when I'm inducting). But since .card = 0 is also used for encoding infinite cardinality, I can't just turn it into .has_card 0 (and thus into a statement that it's an empty set) and have to mess around with some other .finite hypothesis to actually get .has_card 0.

It's definitely doable but it's confused me a bunch of times so I wanted to raise it. I'm not sure what a better option could be though. I understand that I actually need to deal with infinite cases in a bunch of these proofs anyway but maybe it would be less confusing if zero and infinite cardinalities were distinct in the .card value itself. Like a sum type or something.

[Dan Abramov]

I guess maybe part of the confusion is that I can usually do card_to_has_card but it doesn't work for 0 (even if it's finite). However, has_card_card + rw can actually do the job in this case.

[Terence Tao]

In Mathlib there are two different notions of cardinality for precisely this reason: docs#Set.ncard and docs#Set.encard, with the latter taking values in an extension ENat of the natural numbers Nat that also contains an "infinite" element. (Actually, there are bunch of other closely related cardinality notions such as docs#Nat.card, docs#ENat.card, docs#Finset.card, and docs#Fintype.card, but to reduce confusion it's best not to talk about them for now.) I think the choice of which one to use is somewhat application-dependent; but there is so much more API for the natural numbers than the extended natural numbers that it is often more convenient to use a Nat-based cardinality notion even if an ENat version would be conceptually better.

EDIT: in any event, any tips you might have for future students working through Section 3.6 can be added as a PR to the new "tips" section near the start of the Lean file.

[Jireh Loreaux]

Terence Tao said:

but there is so much more API for the natural numbers than the extended natural numbers that it is often more convenient to use a Nat-based cardinality notion even if an ENat version would be conceptually better

I think this is only half the reason the Nat version is more convenient. The other half being that, when everything is finite, you really want to ignore the possibility of anything having infinite cardinality, and so ℕ is honestly conceptually better. This is partly why Finset.card and Fintype.card exist, but those don't work with Finite α assumptions.

[Rado Kirov]

I guess maybe part of the confusion is that I can usually do card_to_has_card but it doesn't work for 0 (even if it's finite). However, has_card_card + rw can actually do the job in this case.

I think I added that theorem, but I can see this variant being more useful

theorem SetTheory.Set.card_to_has_card_fin (X:Set) {n: ℕ} (hfin: X.finite): X.card = n → X.has_card n := by
  rintro rfl
  exact has_card_card hfin

Can send a PR for it too.

[Dan Abramov]

I sent a PR in https://github.com/teorth/analysis/pull/331 with what I personally found helpful.

Rado Kirov said:

I think I added that theorem, but I can see this variant being more useful

Interestingly I had that too but ended up not having use for it thanks to lemmas directly dealing with the empty set.

[Terence Tao]

Just for future reference, here is a table that organizes six different ways one can formalize the assertion "$n$ is the cardinality of $X$" in Mathilb, depending on the type and finite nature of X, and whether we want n to be a natural number or permit it to be infinite.

	[Finite X] (n: Nat)	(n: Nat)	(n: ENat)
X is a set	n = Finset.card X	n = Set.ncard X	n = Set.encard X
X is a type	n = Fintype.card X	n = Nat.card X	n = ENat.card X

There is one small lie in this table, which is that to use Finset.card X or Fintype.card X it is not enough for the set or type X to have a Finite instance; it must be a Finset or a Fintype instead, for technical reasons having to do with things like decidable equality and computability that are not particularly important for most mathematical applications. There are a ton of helper lemmas relating these six notions to each other but none of them are particularly interesting. I don't think there is consensus on which cardinality notion is the "best" to use; it depends on the specific application. (For Analysis I, I didn't want to introduce the extended natural numbers at this stage of the text, nor did I want to introduce a set notion with a bundled notion of finiteness, nor did I want to introduce any type theory; so by the process of elimination, this left me with working with a cardinality notion similar to Set.ncard.)

[Alex Meiburg]

For completeness: worth mentioning that all three in the bottom row also function for the top row (by coercing Set to Type); and that there's also n = Cardinal.mk X.