Create set from universal - existential quantifier pair

Stream: new members

[Josha Dekker]

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]

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

[Josha Dekker]

My bad, incorrectly simplified the MWE. Let me correct

[Ruben Van de Velde]

It does, but r ∈ s doesn't

[Josha Dekker]

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]

New version: just let R be all of X.

[Josha Dekker]

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]

That's the axiom of choice!

[Yaël Dillies]

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]

Great, thank you!