Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 17:25 6379d39e

View on Github →

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.

Estimated changes