Zulip Chat Archive

Stream: new members

Topic: Countable analogue of Finset


Josha Dekker (Dec 18 2023 at 16:52):

I'm formalising Lindelöf spaces, but I'm not entirely sure what the 'mathlib way' of generalising 'Finset ι' to '"Countable" ι' would be, e.g. in the following setting:

universe u v

variable {X : Type u}

variable {s t : Set X}
example {ι : Type v} (U : ι  Set X) (assumptions) :  t : Finset ι, (s   i  t, U i) := by sorry

Just writing 'Countable ι' doesn't give the expected result. I currently have ∃ t : Set ι, Countable t \wedge (s ⊆ ⋃ i ∈ t, U i), is that the way to go?

Yaël Dillies (Dec 18 2023 at 16:55):

docs#Finset is "bundled finiteness". docs#Countable and docs#Set.Countable are "unbundled countability".

Ruben Van de Velde (Dec 18 2023 at 16:55):

Do you actually want iota to be countable or should t be a countable set, possibly embedded in an uncountable type?

Josha Dekker (Dec 18 2023 at 17:00):

Whoops, the last Countable iota should have been Countable t, I just changed it. I was hoping there'd be a 'bundled countability', which is why the first mentions in my message contain Countable iota.

Yaël Dillies (Dec 18 2023 at 17:01):

Then it should be t.Countable, not Countable t.

Josha Dekker (Dec 18 2023 at 17:04):

Great, and then continue with \exists t : Set \iota, t.Countable \wedge ... ?

Jireh Loreaux (Dec 18 2023 at 19:24):

I think docs#Denumerable is the true equivalent of docs#Finset for bundled countably infinite sets, but I'm not arguing that's what you want to use here.

Yaël Dillies (Dec 18 2023 at 19:26):

Uh, not really? It would rather be

structure DenSet (α : Type*) where
  carrier : Set α
  denumerable : Denumerable carrier

which doesn't exist

Jireh Loreaux (Dec 18 2023 at 19:27):

Duh, you're right.

Josha Dekker (Dec 21 2023 at 12:40):

Is there a specific reason why we do not have a countable analogue for Finset? I think that the proofs and definitions for Lindelöf spaces that I'm working on in #9107 would be a bit shorter if we had this.

Yaël Dillies (Dec 21 2023 at 12:42):

It would have less (no?) nice computational content and we rarely (never?) care about the lattice of countable sets of a type. In contrast, we care a lot about the lattice of finite sets.

Josha Dekker (Dec 21 2023 at 12:46):

Thank you, I get that the computational aspects are less nice indeed, for me it just meant for me that something that reads as 't : CountableSet X, p t' has to be written as 't : Set X, t.Countable ∧ p t', which was a bit more cumbersome to work with for me (unfolding the 'and' all the time etc)

Yaël Dillies (Dec 21 2023 at 12:47):

That's probably the lesser evil :smile:

Josha Dekker (Dec 21 2023 at 12:49):

Yes, that is most likely true ... thanks!

Eric Wieser (Dec 21 2023 at 13:58):

Yaël Dillies said:

Uh, not really? It would rather be

structure DenSet (α : Type*) where
  carrier : Set α
  denumerable : Denumerable carrier

which doesn't exist

Doesn't this need a Trunc to make it encoding irrelevant?

Yaël Dillies (Dec 21 2023 at 13:59):

Sure. But the point is that mathlib doesn't have it.


Last updated: May 02 2025 at 03:31 UTC