## Stream: maths

### Topic: card

#### Sebastien Gouezel (Feb 03 2019 at 10:04):

Is there already a function associating to any set its cardinality if it is finite, and 0 otherwise? This would be to enable me to write

∃t, finite t ∧ card t ≤ 17


without type classes trickery to convince Lean that t is a fintype. I know I can write

∃t, ∃H: finite t, (@fintype.card t (finite.fintype H)) ≤ 17


but this is not very readable...

#### Mario Carneiro (Feb 03 2019 at 10:14):

You can use cardinal.mk, but the result isn't a nat

#### Mario Carneiro (Feb 03 2019 at 10:22):

It's not hard to define the function you are talking about either... if you define it with enough supporting theorems it seems like a good utility function for mathlib

#### Sebastien Gouezel (Feb 03 2019 at 10:39):

OK, I'll prepare something like that (and interface it with finsets, fintypes, and cardinal.mk). For the name, what about set.card?

#### Mario Carneiro (Feb 03 2019 at 10:44):

it's not really a set thing.. I was just thinking fintype.card'

#### Mario Carneiro (Feb 03 2019 at 10:44):

I guess it has type Type -> nat

#### Mario Carneiro (Feb 03 2019 at 10:48):

noncomputable def fintype.card' (α : Type*) : ℕ :=
by classical; exact
if h : nonempty (fintype α) then @fintype.card α (classical.choice h) else 0


#### Sebastien Gouezel (Feb 03 2019 at 11:16):

Well, it's not really a fintype thing either, as it applies to all Types an not just fintypes.

#### Mario Carneiro (Feb 03 2019 at 11:23):

that's true, although it is defined in terms of fintypes and only actually works on fintypes

#### Kenny Lau (Feb 03 2019 at 19:32):

roption anyone?

#### Chris Hughes (Feb 03 2019 at 19:40):

No point. It still won't be computable, since you need stronger than a proposition. I wouldn't mind the idea of a roption for fintype instead of Prop though.

#### Chris Hughes (Feb 03 2019 at 19:44):

Not sure that would work actually.

#### Sebastien Gouezel (Feb 05 2019 at 13:37):

Finally, I went for cardinal.mk, it works perfectly for what I want to do. Just one question though: I could not find

theorem mk_eq_mk_iff_nonempty_equiv {α β : Type u} :
mk α = mk β ↔ nonempty (α ≃ β) :=
⟨λh, quotient.exact h, λh, quotient.sound h⟩


in the library. Is it because I did not look closely enough, or is it worth adding?

#### Mario Carneiro (Feb 05 2019 at 13:37):

quotient.eq

Yes, of course!

#### Sebastien Gouezel (Feb 05 2019 at 14:05):

In fact a rewrite along ← quotient.eq does not work since there are too many missing type informations. Unless there is a simple solution, I will add the lemma mk_eq_mk_iff_nonempty_equiv.

#### Mario Carneiro (Feb 05 2019 at 14:07):

you want to rewrite with this equality? What are you doing with this?

#### Mario Carneiro (Feb 05 2019 at 14:08):

In cardinal.lean it's pretty much all stuff like refine quotient.sound ⟨function...⟩

#### Sebastien Gouezel (Feb 05 2019 at 14:12):

I need to use some arbitrary bijection between a given finite set and some fin n, where n is the cardinality of my set. See https://github.com/sgouezel/mathlib/blob/b606163512a103ffa2e5acf335d66089b4fd661b/src/topology/metric_space/gromov_hausdorff.lean#L1345

#### Mario Carneiro (Feb 05 2019 at 14:14):

choice is really not necessary there... you can just cases on it

#### Mario Carneiro (Feb 05 2019 at 14:15):

I would skip the mk_eq_mk_iff theorem, prove mk s = mk (fin N) using rw like that, and then cases quotient.exact this to get an equiv

#### Sebastien Gouezel (Feb 05 2019 at 14:22):

Done, thanks.

Last updated: May 11 2021 at 00:31 UTC