mathlib
6379d39e
- feat(data/set/countable): protect lemmas (#15415)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(data/set/countable): protect lemmas (#15415) We protect `set.countable_iff_exists_injective`, `set.countable_iff_exists_surjective`, and `set.countable.to_encodable` in order to avoid clashes with the theorems on the new `countable` typeclass.
Author
vihdzp
Parents
621cf7f2
Loading