Zulip Chat Archive
Stream: general
Topic: coercing finset to set
Kenny Lau (Sep 13 2018 at 06:20):
What is the idiomatic way to coerce a finset to a set?
Mario Carneiro (Sep 13 2018 at 06:20):
...coercion?
Kenny Lau (Sep 13 2018 at 06:22):
and how do I prove that the set is finite?
Mario Carneiro (Sep 13 2018 at 06:23):
finite_to_set
Kenny Lau (Sep 13 2018 at 06:24):
oh it's in the finset namespace lol
Last updated: May 02 2025 at 03:31 UTC