theorem
Set.pairwise_iUnion
{α : Type u_1}
{κ : Sort u_6}
{r : α → α → Prop}
{f : κ → Set α}
(h : Directed (fun x x_1 => 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 => x ⊆ x_1) s)
:
Set.Pairwise (⋃₀ s) r ↔ ∀ (a : Set α), 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 => 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 => 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 : ι) (_ : i ∈ g i'), f i)
(hg : ∀ (i : ι'), i ∈ s → Set.PairwiseDisjoint (g i) f)
:
Set.PairwiseDisjoint (⋃ (i : ι') (_ : 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' : ι') (_ : i' ∈ t), f (i, i'))
(ht : Set.PairwiseDisjoint t fun i' => ⨆ (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' : ι') (_ : i' ∈ t), f (i, i')) ∧ Set.PairwiseDisjoint t fun i' => ⨆ (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)
:
Equivalence between a disjoint bounded union and a dependent sum.
Equations
- Set.biUnionEqSigmaOfDisjoint h = (Equiv.setCongr (_ : ⋃ (x : ι) (_ : x ∈ s), f x = ⋃ (x : ↑s), f ↑x)).trans (Set.unionEqSigmaOfDisjoint (_ : ∀ (x x_1 : ↑s), x ≠ x_1 → Disjoint (f ↑x) (f ↑x_1)))
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 : ι), i ∈ s → Set.Nonempty (f i))
(h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (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 => ⋃ (i : ι) (_ : i ∈ s), f i