union over a chain is pairwise disjoint of elementwise

Stream: Is there code for X?

[Edward van de Meent]

as far as i can tell, we don't have this (but it is good to have for zorn purposes, afaict):

import Mathlib

lemma IsChain.pairwise_disjoint {α β: Type*} [PartialOrder β] [OrderBot β]
    (c : Set (Set α)) (hc : IsChain (· ⊆ ·) c)
    (f : α → β)
    (h: ∀ s ∈ c, s.PairwiseDisjoint f) : (⋃ s ∈ c, s).PairwiseDisjoint f := by
  sorry

[Edward van de Meent]

a bit more context: i'm trying to choose a largest set such that the image under some f is pairwise disjoint (and some other conditions), and trying to apply zorn_subset to get there...

[Edward van de Meent]

for what it's worth, i have a proof, but i feel like there should be a better way...

import Mathlib

lemma IsChain.pairwise_disjoint {α β: Type*} [PartialOrder β] [OrderBot β]
    (c : Set (Set α)) (hc : IsChain (· ⊆ ·) c)
    (f : α → β)
    (h: ∀ s ∈ c, s.PairwiseDisjoint f) : (⋃ s ∈ c, s).PairwiseDisjoint f := by
  -- exact?
  intro x hx y hy hne
  simp only [mem_iUnion, exists_prop] at hx hy
  obtain ⟨sx,hsx⟩ := hx
  obtain ⟨sy,hsy⟩ := hy
  have wlog_setup : sx ≠ sy → sx ⊆ sy ∨ sy ⊆ sx := (hc hsx.left hsy.left ·)
  wlog hsx_sy : sx ⊆ sy
  · rw [onFun_apply]
    symm
    apply this c hc _ h hne.symm sy hsy sx hsx (fun hne' => Or.symm (wlog_setup hne'.symm)) _
    exact (wlog_setup (fun h => hsx_sy (h ▸ (fun _ a => a)))).elim (fun h => (hsx_sy h).elim) id
  exact h sy hsy.left (hsx_sy hsx.right) hsy.right hne

[Bhavik Mehta]

import Mathlib

lemma DirectedOn.pairwise_iUnion₂ {α : Type*} (c : Set (Set α)) (hc : DirectedOn (· ⊆ ·) c)
    (r : α → α → Prop) (h : ∀ s ∈ c, s.Pairwise r) : (⋃ s ∈ c, s).Pairwise r := by
  simp only [Set.Pairwise, Set.mem_iUnion, exists_prop, forall_exists_index, and_imp]
  intro x S hS hx y T hT hy hne
  obtain ⟨U, hU, hSU, hTU⟩ := hc S hS T hT
  exact h U hU (hSU hx) (hTU hy) hne

lemma IsChain.pairwiseDisjoint_iUnion₂ {α β : Type*} [PartialOrder β] [OrderBot β]
    (c : Set (Set α)) (hc : IsChain (· ⊆ ·) c) (f : α → β)
    (h : ∀ s ∈ c, s.PairwiseDisjoint f) : (⋃ s ∈ c, s).PairwiseDisjoint f :=
  hc.directedOn.pairwise_iUnion₂ _ _ h

your original generalises in two ways, and this simplifies the proof too

[Edward van de Meent]

Thanks, that looks a lot better :tada: