We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 98f778c commit a654426Copy full SHA for a654426
1 file changed
Mathlib/Data/Set/Countable.lean
@@ -361,7 +361,7 @@ theorem uncountable_of_countable_compl [Uncountable α] {s : Set α} (hs : sᶜ.
361
s.Uncountable := fun h =>
362
Set.uncountable_univ (α := α) (by simpa using hs.union h)
363
364
-theorem Finite.uncountable_compl [Uncountable α] {s : Set α} (hs : s.Countable) :
+theorem Countable.uncountable_compl [Uncountable α] {s : Set α} (hs : s.Countable) :
365
sᶜ.Uncountable := fun h =>
366
367
0 commit comments