Combining unions with choice functions and an hypothesis

Stream: new members

[Josha Dekker]

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]

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

[Yaël Dillies]

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]

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]

What would you have expected?

[Josha Dekker]

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]

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

[Josha Dekker]

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

[Yaël Dillies]

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]

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

[Josha Dekker]

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]

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]

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]

Try:

    intro x hx
    have := this hx
    apply?

[Josha Dekker]

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!