feat(Data/Set): add Set.Uncountable

[staroperator]

There are Set specialized shortcuts Set.Finite, Set.Infinite and Set.Countable, but lacking Set.Uncountable. I find this useful in #34246.

---

[github-actions]

PR summary 7c260e7c29

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Countable.not_uncountable
+ Countable.uncountable_compl
+ Uncountable
+ Uncountable.diff
+ Uncountable.image
+ Uncountable.infinite
+ Uncountable.mono
+ Uncountable.nonempty
+ Uncountable.nontrivial
+ Uncountable.not_countable
+ Uncountable.of_image
+ Uncountable.range
+ Uncountable.to_subtype
+ aleph0_lt_iff_set_uncountable
+ not_countable_iff_uncountable
+ not_uncountable_iff_countable
+ uncountable_coe_iff
+ uncountable_of_countable_compl
+ uncountable_union
+ uncountable_univ
+ uncountable_univ_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[vihdzp]

Sure, why not.

[joneugster]

One question which arose in a discussion about the simp-question below is whether it is really sensible to add such a definition.

[...] we already have a nice phrasing as ¬s.Countable, I am not convinced it is useful, because it will force us to introduce quite a lot of API for a gain I don't really see.

and

[...] If the concept is really used a lot, and in particular makes it possible to have several lemmas expressed with dot notation, then we should definitely have it. If it's less used, it's less obvious we should have it. For Infinite, it's a natural assumption in many many lemmas so we should definitely have it. For Uncountable, I don't know. [...]

Is there some more motivation you could provide besides the analogy to Infinite?

[staroperator]

Besides analogy, I find I need the result of "removing a countable set from an uncountable set is still countable" (Set.Uncountable.diff) and "any uncountable set is non-empty" (Set.Uncountable.nonempty) in #34246. If I represent this as ¬s.Countable, I can definitely use Set.Countable.of_diff for the former but the latter is not quite easy (grind may help I guess). These are exactly "several lemmas expressed with dot notation" in my feeling.

[staroperator]

Though I agree that "uncountable sets" do not occur in a lot of lemmas. In fact I would likely generalize #34246 to any regular cardinal so this PR may become unnecessary then.

[staroperator]

Another thing I'd like to point out is that besides ¬s.Countable, another way to write "a set is uncountable" is Uncountable s (where s is coerced to a type). They are of course equivalent via Set.countable_coe_iff and not_countable_iff, but I don't think there is one representation that is more canonical than another (while Set.Uncountable would definitely be the most canonical way to say it).

[staroperator]

FYI, I have generalized #34246, so I don't need this PR now. Still, it doesn't harm to introduce such a shortcut.

[vihdzp]

I'm somewhat unsure as to why we even have an Uncountable predicate. I don't believe there's many useful theorems to be stated about it other than ℵ₁ ≤ #α? And considering you were able to generalize your use of it, I think that signals we don't need this either.

[staroperator]

I'm somewhat unsure as to why we even have an Uncountable predicate. I don't believe there's many useful theorems to be stated about it other than ℵ₁ ≤ #α? And considering you were able to generalize your use of it, I think that signals we don't need this either.

I guess Uncountable exists because it's a typeclass. That's useful because instance synthesis automates proof that some complicate type is actually uncountable.

[vihdzp]

There's only three dozen theorems about uncountable, and most are just boilerplate conversions. I don't think anyone would miss this typeclass if it were gone.

[joneugster]

Thanks for the motivation. I personally don't see anything against introducing it and the analogy to all the other declarations listed seems already reasonably compelling to me.

I'll leave this to the maintainer to decide; for context: #mathlib reviewers > @[simp] @ 💬

maintainer merge?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[vihdzp]

I'm increasingly convinced that we don't want this, and furthermore, that we don't want Uncountable either.

I've opened a Zulip thread for discussion.

[joneugster]

@staroperator if the zulip discussion has been fruitful, could you please act on it or write about the conclusion here and remove the label by commenting -awaiting-zulip (I think it needs to be on its own line, maybe a separate message)

[staroperator]

@staroperator if the zulip discussion has been fruitful, could you please act on it or write about the conclusion here and remove the label by commenting -awaiting-zulip (I think it needs to be on its own line, maybe a separate message)

Thanks for the reminder. I guess the conclusion is that Uncountable is still useful for some theorems, and there is no need to remove it.

There is no discussion about whether Set.Uncountable should be introduced, but feel free to continue the discussion in the Zulip thread above.

-awaiting-zulip

[joneugster]

So far I've only heard the opinion of @vihdzp and @sgouezel voicing concerns that the API Set.Uncountable is useful, so I'm hesitant on moving this further without stronger evidence that this is useful.

If you believe it to be useful, it would be nice if you could take the initiative of gathering such evidence.

meanwhile I'm going to unassign myself for now. This should mean other people might see the PR and voice their opinion.

[staroperator]

So far I've only heard the opinion of @vihdzp and @sgouezel voicing concerns that the API Set.Uncountable is useful, so I'm hesitant on moving this further without stronger evidence that this is useful.

If you believe it to be useful, it would be nice if you could take the initiative of gathering such evidence.

meanwhile I'm going to unassign myself for now. This should mean other people might see the PR and voice their opinion.

Actually, I'm also not sure whether introducing this is useful now, so I will close the PR.