# Zulip Chat Archive

## 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`

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

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