Zulip Chat Archive

Stream: Is there code for X?

Topic: Not countable

Josha Dekker (Dec 23 2023 at 12:28):

Do we have a Class for Uncountable (i.e. strictly larger cardinality than Countable), or should I just use \neg (Countable ...) to encode this information?

Riccardo Brasca (Dec 23 2023 at 12:31):

We use ¬ Countable, see for example docs#not_countable_complex.

Riccardo Brasca (Dec 23 2023 at 12:32):

But this is not a crazy idea, we have for example docs#Set.Subsingleton and docs#Set.Nontrivial

Yury G. Kudryashov (Dec 23 2023 at 14:46):

IMHO, we should have a class for Uncountable and Filter.cocountable.

Josha Dekker (Dec 23 2023 at 14:58):

I’m working on Filter.cocountable, see my message earlier today: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Cocountable.20filter/near/409699987

Josha Dekker (Dec 23 2023 at 14:59):

Or do you mean that Filter.cocountable should make use of the class Uncountable explicitly?

Yury G. Kudryashov (Dec 23 2023 at 15:02):

It should use it for instance [Uncountable α] : NeBot (cocountable α)

Yury G. Kudryashov (Dec 23 2023 at 15:02):

(or cocountable : Filter α, if you make α implicit)

Josha Dekker (Dec 23 2023 at 15:09):

Yury G. Kudryashov said:

It should use it for instance [Uncountable α] : NeBot (cocountable α)

Yes, that’s where I have a little problem now, as I didn’t know how to write what would boil down to [\neg Countable \alpha]. I skipped that part for now, but I could make a class here that is defined similar to Countable, but with a negation and leave it in Filter.cocountable for now?

Yury G. Kudryashov (Dec 23 2023 at 15:15):

You should create a new file near the definition of docs#Countable with

@[mk_iff]
class Uncountable (α : Sort*) : Prop where
  not_countable : ¬Countable α

lemmas like Function.Injective.uncountable, Function.Surjective.uncountable, and instances like

instance [Uncountable α] : Uncountable (α ⊕ β] :=
  Sum.inl_injective.uncountable

Yury G. Kudryashov (Dec 23 2023 at 15:17):

Probably, you should PR the Uncountable class first, then Filter.cocountable.

Yury G. Kudryashov (Dec 23 2023 at 15:17):

Or you can PR the Filter.cocountable without the NeBot instance, then PR the Uncountable class.

Josha Dekker (Dec 23 2023 at 15:18):

I need to keep the PR’s small anyway, I’ll see what I can do soon! Can I @ you as reviewer once I make the PR’s?

Yaël Dillies (Dec 23 2023 at 15:20):

I think it should be in the same file as Countable

Yury G. Kudryashov (Dec 23 2023 at 15:23):

We already have 3 files in Data/Countable.

Yaël Dillies (Dec 23 2023 at 15:24):

I maintain. The negation of a property should be in the same file as that property.

Yury G. Kudryashov (Dec 23 2023 at 15:25):

Then a good way is to mirror each statement about Countable with a statement about Uncountable.

Josha Dekker (Dec 23 2023 at 15:40):

Okay, I'll work on a PR for a bit!

Josha Dekker (Dec 23 2023 at 15:46):

Just to make sure I get this right, I need to add it to Data/Countable/Defs.lean, right?

Yury G. Kudryashov (Dec 23 2023 at 15:50):

And possibly add some lemmas to Data/Countable/Basic

Josha Dekker (Dec 24 2023 at 07:29):

This is now #9254. It is very small at this point, I'd like to make sure I get it right before adding more API, so any feedback is welcome!

Yury G. Kudryashov (Dec 24 2023 at 15:34):

BTW, should we define Uncountable for Sort* or for Type*? All instances will be in Type* and assuming Type* can make it easier for Lean to unify universes (am I right?).

Josha Dekker (Dec 24 2023 at 15:58):

I just went for the same option as Countable to ensure consistency, I’m happy to change it though! Perhaps we should change both of them then?

Yury G. Kudryashov (Dec 24 2023 at 16:04):

No, (p : Prop) : Countable p is a valid instance.

Yury G. Kudryashov (Dec 24 2023 at 16:04):

But proofs of a proposition form a Subsingleton, hence finite, hence countable.

Yury G. Kudryashov (Dec 24 2023 at 16:05):

I pushed some changes to your branch.

Yury G. Kudryashov (Dec 24 2023 at 16:16):

@Mario Carneiro Are there any reasons to use Sort* for Uncountable? If no, then should we change Infinite to Type* too?

Mario Carneiro (Dec 24 2023 at 16:18):

Well they are propositions, you are allowed to negate them too

Mario Carneiro (Dec 24 2023 at 16:18):

But I agree it's not much use to have either Countable or Uncountable as working on Sort*

Mario Carneiro (Dec 24 2023 at 16:19):

I would probably just put them in Type* until some use case actually needs them to be Sort*

Yury G. Kudryashov (Dec 24 2023 at 16:20):

Countable is useful on Sort* because we can apply lemmas like docs#MeasureTheory.measure_iUnion_null to a Countable Sort*

Yury G. Kudryashov (Dec 24 2023 at 16:20):

(BTW, we should change this lemma to use Sort*)

Kevin Buzzard (Dec 24 2023 at 16:21):

Looking forward to PUncountable in the future :-)

Yury G. Kudryashov (Dec 24 2023 at 16:21):

Why would you need this?

Kevin Buzzard (Dec 24 2023 at 16:22):

Well you just pointed out that Countable was useful on Sort*, so I'm just waiting for the future use case :-)

Mario Carneiro (Dec 24 2023 at 16:22):

Right back at you, given that the lemma doesn't actually work on Sort* today it doesn't seem to support your argument that we need it

Mario Carneiro (Dec 24 2023 at 16:23):

There is a TODO about it two lemmas down though

Mario Carneiro (Dec 24 2023 at 16:24):

but it seems that it was provable just the same, so it doesn't seem to be essential to unify them

Josha Dekker (Dec 24 2023 at 16:24):

Yury G. Kudryashov said:

I pushed some changes to your branch.

Thanks, feel free to add more of course!

Yury G. Kudryashov (Dec 24 2023 at 16:27):

Right, we have separate lemmas for unions over Type*s and Props. When we introduced Countable, the plan was to unify them, but then we forgot.

Yury G. Kudryashov (Dec 24 2023 at 16:28):

We definitely use this trick for Finite and docs#Filter.eventually_all

Mario Carneiro (Dec 24 2023 at 16:29):

yes I remember, that was where one of the spurious universe bumps in mathlib came from

Yury G. Kudryashov (Dec 24 2023 at 16:39):

How does this lead to a universe bump?

Yury G. Kudryashov (Dec 24 2023 at 16:40):

There was a bump when I made docs#finprod work for Sort*s using PLift.

Mario Carneiro (Dec 24 2023 at 16:40):

I think the construction uses PLift, which lifts things in Sort u to Type u

Yury G. Kudryashov (Dec 24 2023 at 16:41):

Maybe some instances use PLift but not the definition.

Mario Carneiro (Dec 24 2023 at 16:42):

oh I see, I guess the definition is no longer Nonempty (Fintype A)

Yury G. Kudryashov (Dec 24 2023 at 16:43):

Yes, the definition is ∃ n, Nonempty (α ≃ Fin n)

Mario Carneiro (Dec 24 2023 at 16:44):

I don't really mind one way or another, do what you prefer

Yury G. Kudryashov (Dec 24 2023 at 16:45):

I think that we'll go with Sort* in this PR, then I'll try to change Infinite and Uncountable to Type* in another PR.

Yury G. Kudryashov (Dec 24 2023 at 16:46):

BTW, do we need Classical.choice for this?

import Mathlib

lemma {α : Type*} {π : α → Type*} [Infinite α] [∀ a, Nontrivial (π a)] : ¬Countable ((a : α) → π a) := _

Yury G. Kudryashov (Dec 24 2023 at 16:47):

I guess, yes, because of the way we define Infinite (at least)

Mario Carneiro (Dec 24 2023 at 16:48):

is nontrivial constructive?

Yury G. Kudryashov (Dec 24 2023 at 16:48):

No, it's a Prop

Yury G. Kudryashov (Dec 24 2023 at 16:48):

And Infinite is very non-constructive: it's Not (Finite α).

Mario Carneiro (Dec 24 2023 at 16:48):

in that case yes, it's equivalent to the axiom of choice

Yury G. Kudryashov (Dec 24 2023 at 16:48):

So, the answer is "not" and I can use choose in the proof.

Mario Carneiro (Dec 24 2023 at 16:49):

without choice you can't even prove that type is nonempty

Josha Dekker (Jan 04 2024 at 20:04):

Shall I put #9254 out for review, or should something new be added there?

Last updated: May 02 2025 at 03:31 UTC