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