basic): lemmas about `finset.univ` (#17067)

Commit

3 years ago

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`.

Author

urkud

Parents

8308d266

mathlib3 5155be47 - feat(data/fintype/basic): lemmas about `finset.univ` (#17067)

mathlib3
5155be47 - feat(data/fintype/basic): lemmas about `finset.univ` (#17067)