Why Uncountable

Stream: mathlib4

[Violeta Hernández]

There are currently 38 declarations mentioning docs#Uncountable. None of them are particularly interesting - they're just boilerplate linking it to docs#Small or docs#Countable or docs#Infinite. More pointedly, we don't really have any major theorem that requires this assumption.

Does this show a lack of API? Or does it show that we have no use of this predicate as anything separate than ¬ Countable α?

[Eric Wieser]

I think the answer is that it's useful because it's a typeclass and so inferred automatically?

[Eric Wieser]

At least, that's why it is more useful than ¬ Countable α

[Violeta Hernández]

Well, we don't seem to need to infer it anywhere

[Jireh Loreaux]

You could have this theorem:

lemma {α : Type*} [Uncountable α] {f : α → ℝ≥0∞} (hf : ∀ x, 0 < f x) : ∑' x, f x = ∞ := by sorry

[Dexin Zhang]

Jireh Loreaux said:

You could have this theorem:

lemma {α : Type*} [Uncountable α] {f : α → ℝ≥0∞} (hf : ∀ x, 0 < f x) : ∑' x, f x = ∞ := by sorry

Shouldn't this hold for Infinite α already?

[Violeta Hernández]

1 + 1/2 + 1/4 + 1/8 + ...

[Violeta Hernández]

I guess docs#Uncountable could be useful in measure theory

[Dexin Zhang]

Seems some statements in model theory used ℵ₀ < #K in their assumption.

[Snir Broshi]

Jireh Loreaux said:

You could have this theorem:

Can't we generalize to:

import Mathlib
open Cardinal
lemma foo {α β : Type*} [AddCommMonoid β] [TopologicalSpace β] [CompleteLattice β]
    (h : Nonempty (β ↪ α)) {f : α → β} (hf : 0 < f) : tsum f = ⊤ := by
  sorry

(perhaps with some extra typeclasses, such as OrderTopology β)

[Dexin Zhang]

And there are some statements on Borel spaces using ¬ Countable.

[Aaron Liu]

Snir Broshi said:

Jireh Loreaux said:

You could have this theorem:

Can't we generalize to:

import Mathlib
open Cardinal
lemma foo {α β : Type*} [AddCommMonoid β] [TopologicalSpace β] [CompleteLattice β]
    (h : Nonempty (β ↪ α)) {f : α → β} (hf : 0 < f) : tsum f = ⊤ := by
  sorry

(perhaps with some extra typeclasses, such as OrderTopology β)

it's not more general, since knowing that the reals inject into every uncountable type is the continuum hypothesis

[Violeta Hernández]

Dexin Zhang said:

And there are some statements on Borel spaces using ¬ Countable.

Alright, I think I'm convinced that this is a lack of API and not a lack of interesting results.

[David Michael Roberts]

Uncountable regular cardinals or uncountable strong limit cardinals are useful (all three conditions give inaccessibility, but only in pairs gives many interesting examples in ZFC).