Zulip Chat Archive
Stream: new members
Topic: cardinality of image set of a function
Arthur Paulino (Nov 05 2021 at 21:23):
how do I define a function that returns the cardinality of the image set of a function?
Eric Wieser (Nov 05 2021 at 21:25):
docs#cardinal.mk? So #(set.range f) maybe?
Kyle Miller (Nov 05 2021 at 21:31):
If everything is finite, you might be wanting finset.card (finset.image f finset.univ)
Last updated: May 02 2025 at 03:31 UTC