## Stream: new members

### Topic: Combining unions with choice functions and an hypothesis

#### Josha Dekker (Dec 19 2023 at 13:07):

One more question, I have defined a choice function 'r' and would like to take the union over the function applications on a set, i.e. {r s | s in S}. However, 'r' needs that s in S; how do I feed it this information? The example in the MWE does not work.

universe u v
variable {X : Type u} {ι : Type v}

variable {s t : Set X} {S : Set (Set X)}
variable {r : (s : Set X) → s ∈ S → Set ι}

example : ⋃ (s : Set X) (hs : s ∈ S), r s hs := sorry


#### Yaël Dillies (Dec 19 2023 at 13:09):

Note this is not a MWE because if I paste it in an empty file I get unknown identifier "Set".

#### Yaël Dillies (Dec 19 2023 at 13:09):

import Mathlib.Data.Set.Lattice

universe u v
variable {X : Type u} {ι : Type v}

variable {s t : Set X} {S : Set (Set X)}
variable {r : (s : Set X) → s ∈ S → Set ι}

example : ⋃ (s : Set X) (hs : s ∈ S), r s hs := sorry


works for me

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

Oops, forgot the top line indeed. The definition works, but if you unfold it, you see that lean treats the example as 'union over s, union over hs, r s hs', which I think is not correct?

#### Yaël Dillies (Dec 19 2023 at 13:12):

What would you have expected?

#### Josha Dekker (Dec 19 2023 at 13:14):

intuitively, I would expect to have 'union over s in S, r s', where lean uses (s in S) to eliminate that hypothesis from r, if you get what I mean?

#### Kevin Buzzard (Dec 19 2023 at 13:14):

Taking a union over proofs is counterintuitive but logically equivalent to what you're writing.

#### Josha Dekker (Dec 19 2023 at 13:15):

Okay, then I'll probably need to do something different in the proof I'm writing! Thanks!

#### Yaël Dillies (Dec 19 2023 at 13:21):

This is a tricky question. The above is correct only because Set X is a complete lattice, not merely conditionally complete like ℝ.

#### Yaël Dillies (Dec 19 2023 at 13:22):

I don't think you need to change anything to the proof you're writing. The above is correct and idiomatic.

#### Josha Dekker (Dec 19 2023 at 13:25):

I see that using choose! instead of choose to define r in the first place got rid of the part (s in S), which was what I needed; I think that is somewhat easier to work with in my situation rather than the 'double union'

#### Josha Dekker (Dec 20 2023 at 08:40):

I've been playing around a bit with a reduced version of the problem that I need to prove, but I can't quite seem to get it right in Lean / I can't figure out how to prove the last sorry, perhaps my construction (what I "use") is not the thing I should be using? The 'refine' statements were produced by running "apply?". Any pointers on how to proceed?

import Mathlib.Data.Set.Countable
open Set

universe u v
variable {X : Type u} {ι : Type v}

variable {s t : Set X}

theorem aux {ι : Type v} (U : ι → Set X)
(hsU : s ⊆ ⋃ i, U i) :
∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, ∃ r : Set ι, r.Countable ∧ (s ⊆ ⋃ i ∈ r, U i))
→ ∃ r : Set ι, r.Countable ∧ (⋃ s ∈ S, s ⊆ ⋃ i ∈ r, U i) := by
intro S hS hsr
choose! r hr using hsr
use ⋃ s ∈ S, r s
constructor
· refine (Countable.biUnion_iff hS).mpr ?h.left.a
intro s hs
apply (hr s hs).1
· refine iUnion_subset ?h.right.h
intro i
simp
intro is
have := (hr i is).2
sorry


#### Josha Dekker (Dec 20 2023 at 08:43):

In math terms, I use the fact that a countable union of countable sets (the r(s)) remains countable; both countability of 'r' constructed in this way and the fact that each element of the union over (s in S) is included in one of the unions over countable sets provides the desired result.

#### Ruben Van de Velde (Dec 20 2023 at 09:18):

Try:

    intro x hx
have := this hx
apply?


#### Josha Dekker (Dec 20 2023 at 09:26):

Thanks, that worked! That was the last missing piece of the puzzle that shows that the definition of a Lindelöf space in terms of filters indeed guarantees the countable subcover property, so I'll probably make a PR for that soon!

Last updated: Dec 20 2023 at 11:08 UTC