Commit 2023-11-02 11:46 3a5265f9
View on Github →feat: bijective_iff_map_univ_eq_univ (#7120) For functions on finite sets, they are bijections iff they map universes into universes.
feat: bijective_iff_map_univ_eq_univ (#7120) For functions on finite sets, they are bijections iff they map universes into universes.