card

Stream: maths

[Sebastien Gouezel]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

I guess it has type Type -> nat

[Mario Carneiro]

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

[Sebastien Gouezel]

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

[Mario Carneiro]

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

[Kenny Lau]

roption anyone?

[Chris Hughes]

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]

Not sure that would work actually.

[Sebastien Gouezel]

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]

quotient.eq

[Sebastien Gouezel]

Yes, of course!

[Sebastien Gouezel]

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]

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

[Mario Carneiro]

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

[Sebastien Gouezel]

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]

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

[Mario Carneiro]

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]

Done, thanks.