cardinality of a finite set?

Stream: general

[Scott Morrison]

Sorry, basic question:

If I have (w : set M) (f : w.finite), how am I supposed to refer to the cardinality of this set?

I wish it were possible (e.g. by making set.finite a class) to just provide a fintype instance for the coercion to type, and write fintype.card w.

[Eric Rodriguez]

seems like docs#set.finite.fintype is a thing, but for the same reason as what you said it's not an instance

[Eric Rodriguez]

there's also docs#set.finite.to_finset, and I'd really hope that those two cardinalities are defeq

[Eric Wieser]

Making docs#set.finite a class would be somewhat pointless, as then it would basically just be fintype s

[Kevin Buzzard]

fincard!

[Sebastien Gouezel]

No, because fintype has data (so, diamonds), while finite doesn't.

[Kevin Buzzard]

If we didn't make fincard yet, its definition should be finsum w 1

[Eric Rodriguez]

Eric Rodriguez said:

there's also docs#set.finite.to_finset, and I'd really hope that those two cardinalities are defeq

they don't seem to be

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/group-theory-game/blob/152ec4a92ad67b6174a3d240c63fa56a6df6017e/src/finsum/basic.lean#L290

[Kevin Buzzard]

Oh darn, it's for finite types :-(

[Eric Wieser]

Is there a lemma about docs#cardinal.to_nat and set.finite?

[Eric Wieser]

I guess you can use docs#cardinal.lt_omega_iff_finite with something like docs#cardinal.cast_to_nat_of_lt_omega

[Yakov Pechersky]

Aaron Anderson made a nat.card, which is fincard

[Yakov Pechersky]

You can use that or set.finite.to_finset.card