Commit 2024-11-07 13:47 d08f234e

View on Github →

feat: cardinality of the graph of a function (#18401) From PFR

Estimated changes

added theorem Set.ncard_graphOn
added theorem Set.natCard_graphOn
added theorem Set.natCard_pos