theorem
Set.pairwise_iUnion
{α : Type u_1}
{κ : Sort u_6}
{r : α → α → Prop}
{f : κ → Set α}
(h : Directed (fun (x x_1 : Set α) => x ⊆ x_1) f)
:
Set.Pairwise (⋃ (n : κ), f n) r ↔ ∀ (n : κ), Set.Pairwise (f n) r
theorem
Set.pairwise_sUnion
{α : Type u_1}
{r : α → α → Prop}
{s : Set (Set α)}
(h : DirectedOn (fun (x x_1 : Set α) => x ⊆ x_1) s)
:
Set.Pairwise (⋃₀ s) r ↔ ∀ a ∈ s, Set.Pairwise a r
theorem
Set.pairwiseDisjoint_iUnion
{α : Type u_1}
{ι : Type u_4}
{ι' : Type u_5}
[PartialOrder α]
[OrderBot α]
{f : ι → α}
{g : ι' → Set ι}
(h : Directed (fun (x x_1 : Set ι) => x ⊆ x_1) g)
:
Set.PairwiseDisjoint (⋃ (n : ι'), g n) f ↔ ∀ ⦃n : ι'⦄, Set.PairwiseDisjoint (g n) f
theorem
Set.pairwiseDisjoint_sUnion
{α : Type u_1}
{ι : Type u_4}
[PartialOrder α]
[OrderBot α]
{f : ι → α}
{s : Set (Set ι)}
(h : DirectedOn (fun (x x_1 : Set ι) => x ⊆ x_1) s)
:
Set.PairwiseDisjoint (⋃₀ s) f ↔ ∀ ⦃a : Set ι⦄, a ∈ s → Set.PairwiseDisjoint a f
theorem
Set.PairwiseDisjoint.biUnion
{α : Type u_1}
{ι : Type u_4}
{ι' : Type u_5}
[CompleteLattice α]
{s : Set ι'}
{g : ι' → Set ι}
{f : ι → α}
(hs : Set.PairwiseDisjoint s fun (i' : ι') => ⨆ i ∈ g i', f i)
(hg : ∀ i ∈ s, Set.PairwiseDisjoint (g i) f)
:
Set.PairwiseDisjoint (⋃ i ∈ s, g i) f
Bind operation for Set.PairwiseDisjoint. If you want to only consider finsets of indices, you
can use Set.PairwiseDisjoint.biUnion_finset.
theorem
Set.PairwiseDisjoint.prod_left
{α : Type u_1}
{ι : Type u_4}
{ι' : Type u_5}
[CompleteLattice α]
{s : Set ι}
{t : Set ι'}
{f : ι × ι' → α}
(hs : Set.PairwiseDisjoint s fun (i : ι) => ⨆ i' ∈ t, f (i, i'))
(ht : Set.PairwiseDisjoint t fun (i' : ι') => ⨆ i ∈ s, f (i, i'))
:
Set.PairwiseDisjoint (s ×ˢ t) f
If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is
pairwise disjoint. Not to be confused with Set.PairwiseDisjoint.prod.
theorem
Set.pairwiseDisjoint_prod_left
{α : Type u_1}
{ι : Type u_4}
{ι' : Type u_5}
[Order.Frame α]
{s : Set ι}
{t : Set ι'}
{f : ι × ι' → α}
:
Set.PairwiseDisjoint (s ×ˢ t) f ↔ (Set.PairwiseDisjoint s fun (i : ι) => ⨆ i' ∈ t, f (i, i')) ∧ Set.PairwiseDisjoint t fun (i' : ι') => ⨆ i ∈ s, f (i, i')
noncomputable def
Set.biUnionEqSigmaOfDisjoint
{α : Type u_1}
{ι : Type u_4}
{s : Set ι}
{f : ι → Set α}
(h : Set.PairwiseDisjoint s f)
:
↑(⋃ i ∈ s, f i) ≃ (i : ↑s) × ↑(f ↑i)
Equivalence between a disjoint bounded union and a dependent sum.
Equations
- Set.biUnionEqSigmaOfDisjoint h = (Equiv.setCongr ⋯).trans (Set.unionEqSigmaOfDisjoint ⋯)
Instances For
theorem
Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion
{α : Type u_1}
{ι : Type u_4}
{f : ι → Set α}
{s : Set ι}
{t : Set ι}
(h₀ : Set.PairwiseDisjoint (s ∪ t) f)
(h₁ : ∀ i ∈ s, Set.Nonempty (f i))
(h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i)
:
s ⊆ t
theorem
Pairwise.biUnion_injective
{α : Type u_1}
{ι : Type u_4}
{f : ι → Set α}
(h₀ : Pairwise (Disjoint on f))
(h₁ : ∀ (i : ι), Set.Nonempty (f i))
:
Function.Injective fun (s : Set ι) => ⋃ i ∈ s, f i