Countable analogue of Finset

Stream: new members

[Josha Dekker]

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]

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

[Ruben Van de Velde]

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

[Josha Dekker]

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]

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

[Josha Dekker]

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

[Jireh Loreaux]

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]

Uh, not really? It would rather be

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

which doesn't exist

[Jireh Loreaux]

Duh, you're right.

[Josha Dekker]

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]

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]

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]

That's probably the lesser evil :smile:

[Josha Dekker]

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

[Eric Wieser]

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]

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