## Stream: new members

### Topic: Create set from universal - existential quantifier pair

#### Josha Dekker (Dec 19 2023 at 11:00):

I'd like to know how to tackle the following problem: I have a set S, and know that for each element of this set, there is some r such that a given property holds. I would then like to create a new set by taking the union over S:

universe u v

variable {X : Type u} {S : Set (Set X)}

example (hsr : ∀ s ∈ S, (∃ r : Set X, r.Countable ∧ Nonempty (r.inter s))) : ∃ R : Set X, ∀ s ∈ S, Nonempty (R.inter s)  := sorry


It is slightly rephrased to get a workable MWE, so I'm only interested in constructing the set R efficiently, as
R = {r | r follows from hsr applied to s}.

#### Kevin Buzzard (Dec 19 2023 at 11:04):

I'm surprised p r typechecks. And I'm surprised r \in s typechecks.On phone so can't check...

#### Josha Dekker (Dec 19 2023 at 11:06):

My bad, incorrectly simplified the MWE. Let me correct

#### Ruben Van de Velde (Dec 19 2023 at 11:06):

It does, but r ∈ s doesn't

#### Josha Dekker (Dec 19 2023 at 11:11):

Updated the original message, this typechecks now. My question is on a clean way of defining R, because this statement will not be true in general.

#### Kevin Buzzard (Dec 19 2023 at 11:23):

New version: just let R be all of X.

#### Josha Dekker (Dec 19 2023 at 11:31):

Right, I didn't add the countability hypothesis to R indeed. My actual question is: How to write R = {r | r follows from hsr applied to s, s in S} in Lean?

#### Yaël Dillies (Dec 19 2023 at 11:33):

That's the axiom of choice!

#### Yaël Dillies (Dec 19 2023 at 11:34):

See docs#Classical.axiom_of_choice. If you're within a proof, you can use the tactic choose, as in choose R hR using hsr.

#### Josha Dekker (Dec 19 2023 at 11:35):

Great, thank you!

Last updated: Dec 20 2023 at 11:08 UTC