Commit 2022-10-26 13:26 5155be47

View on Github →

feat(data/fintype/basic): lemmas about finset.univ (#17067) Add finset.ssubset_univ_iff, set.to_finset_eq_univ, and set.to_finset_ssubset_univ.

Estimated changes

Modified src/data/fintype/basic.lean

added theorem finset.ssubset_univ_iff

added theorem set.to_finset_eq_univ

added theorem set.to_finset_ssubset_univ