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.