bigger range of an iUnion

Stream: Is there code for X?

[Pedro Sánchez Terraf]

Do we have this in mathlib?

import Mathlib.SetTheory.Cardinal.Ordinal

open Set

lemma mem_iUnion_of_implies {A : α → Set β} {P Q : α → Prop} (hx : x ∈ ⋃ (j) (_ : P j), A j)
    (hPQ : ∀ j, P j → Q j) : x ∈ ⋃ (j) (_ : Q j), A j := by
  rw [mem_iUnion] at *
  cases' hx with j hj
  rw [mem_iUnion] at hj
  cases' hj with i hi
  exists j
  rw [mem_iUnion]
  exists (hPQ j i)

(I'm also interested in any comment regarding style, naming convention, more idiomatic proof, etc.)
My use case is for

example {A : Ordinal → Set β} {i : Ordinal} (hx : x ∈ ⋃ j < i, A j) (hik : i < k) :
    x ∈ ⋃ j < k, A j := mem_iUnion_of_implies hx (λ j a ↦ gt_trans hik a)

(Not sure if this is somewhat related to Kyle's recent PR...)

[Anatole Dedecker]

docs#Set.biUnion_mono is a more general statement, but it’s written for sets instead of predicates

[Pedro Sánchez Terraf]

Right, the thing is trying to avoid going through Iio i and Iio k (the corresponding sets), since in practice one uses ordinal indices like in the example. The idea is to have some API for ordinal-indexed operations.

What would be an appropriate name for the lemma?

[Kyle Miller]

(That PR you linked to is only for sums/products; unions use a different notation since they don't need to worry about whether the domain is a Finset)

[Kyle Miller]

If you're willing to have α be a Type rather than a Sort, then you can go through Anatole's suggestion:

lemma mem_iUnion_of_implies (α : Type _) {A : α → Set β} {P Q : α → Prop}
    (hPQ : ∀ j, P j → Q j) : ⋃ (j) (_ : P j), A j ⊆ ⋃ (j) (_ : Q j), A j := by
  change ⋃ (j ∈ setOf P), A j ⊆ ⋃ (j ∈ setOf Q), A j
  apply biUnion_mono hPQ
  intros
  exact Subset.rfl

[Pedro Sánchez Terraf]

Kyle Miller said:

If you're willing to have α be a Type rather than a Sort, then you can go through Anatole's suggestion:

Thank you very much! Yes, that would not be a problem---it seems that the general lemma might not be very interesting . As I said, my main interest is to streamline the use of ordinal indices.

[Kyle Miller]

Here's another short proof, without that constraint.

lemma mem_iUnion_of_implies {A : α → Set β} {P Q : α → Prop}
    (hPQ : ∀ j, P j → Q j) : ⋃ (j) (_ : P j), A j ⊆ ⋃ (j) (_ : Q j), A j := by
  apply iUnion₂_mono'
  intro i hi
  exists i
  exists (hPQ i hi)

[Kyle Miller]

Or a one-liner:

lemma mem_iUnion_of_implies {A : α → Set β} {P Q : α → Prop}
    (hPQ : ∀ j, P j → Q j) : ⋃ (j) (_ : P j), A j ⊆ ⋃ (j) (_ : Q j), A j :=
  iUnion₂_mono' fun i hi => ⟨i, hPQ i hi, Subset.rfl⟩

[Kyle Miller]

example {A : Ordinal → Set β} {i : Ordinal} (hik : i < k) :
    ⋃ j < i, A j ⊆ ⋃ j < k, A j :=
  iUnion₂_mono' fun i hi => ⟨i, gt_trans hik hi, Subset.rfl⟩

[Pedro Sánchez Terraf]

Great, so it was Set.iUnion₂_mono' (I couldn't make the linkifier work for that name :sweat_smile: ).
Thank you very much!