Pairwise results for chains

In this file Pairwise results are applied to chains of sets.

theorem IsChain.pairwise_iUnion₂ {α : Type u_1} {c : Set (Set α)} {r : α → α → Prop} (hc : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c) : (⋃ s ∈ c, s).Pairwise r ↔ ∀ s ∈ c, s.Pairwise r

theorem IsChain.pairwiseDisjoint_iUnion₂ {α : Type u_1} {β : Type u_2} {c : Set (Set α)} (hc : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c) [PartialOrder β] [OrderBot β] (f : α → β) : (⋃ s ∈ c, s).PairwiseDisjoint f ↔ ∀ s ∈ c, s.PairwiseDisjoint f

theorem IsChain.pairwise_sUnion {α : Type u_1} {c : Set (Set α)} {r : α → α → Prop} (hc : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c) : (⋃₀ c).Pairwise r ↔ ∀ s ∈ c, s.Pairwise r

theorem IsChain.pairwiseDisjoint_sUnion {α : Type u_1} {β : Type u_2} {c : Set (Set α)} (hc : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c) [PartialOrder β] [OrderBot β] (f : α → β) : (⋃₀ c).PairwiseDisjoint f ↔ ∀ s ∈ c, s.PairwiseDisjoint f