theorem
Set.pairwise_iUnion₂
{α : Type u_1}
{s : Set (Set α)}
(hd : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s)
(r : α → α → Prop)
(h : ∀ a ∈ s, a.Pairwise r)
:
(⋃ a ∈ s, a).Pairwise r
theorem
Set.pairwise_iUnion₂_iff
{α : Type u_1}
{r : α → α → Prop}
{s : Set (Set α)}
(hd : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s)
:
theorem
Set.pairwise_sUnion
{α : Type u_1}
{r : α → α → Prop}
{s : Set (Set α)}
(hd : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s)
:
theorem
Set.pairwiseDisjoint_iUnion
{α : Type u_1}
{ι : Type u_2}
{ι' : Type u_3}
[PartialOrder α]
[OrderBot α]
{f : ι → α}
{g : ι' → Set ι}
(h : Directed (fun (x1 x2 : Set ι) => x1 ⊆ x2) g)
:
(⋃ (n : ι'), g n).PairwiseDisjoint f ↔ ∀ ⦃n : ι'⦄, (g n).PairwiseDisjoint f
theorem
Set.pairwiseDisjoint_sUnion
{α : Type u_1}
{ι : Type u_2}
[PartialOrder α]
[OrderBot α]
{f : ι → α}
{s : Set (Set ι)}
(h : DirectedOn (fun (x1 x2 : Set ι) => x1 ⊆ x2) s)
:
(⋃₀ s).PairwiseDisjoint f ↔ ∀ ⦃a : Set ι⦄, a ∈ s → a.PairwiseDisjoint f
theorem
Set.PairwiseDisjoint.biUnion
{α : Type u_1}
{ι : Type u_2}
{ι' : Type u_3}
[CompleteLattice α]
{s : Set ι'}
{g : ι' → Set ι}
{f : ι → α}
(hs : s.PairwiseDisjoint fun (i' : ι') => ⨆ i ∈ g i', f i)
(hg : ∀ i ∈ s, (g i).PairwiseDisjoint f)
:
(⋃ i ∈ s, g i).PairwiseDisjoint 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_2}
{ι' : Type u_3}
[CompleteLattice α]
{s : Set ι}
{t : Set ι'}
{f : ι × ι' → α}
(hs : s.PairwiseDisjoint fun (i : ι) => ⨆ i' ∈ t, f (i, i'))
(ht : t.PairwiseDisjoint fun (i' : ι') => ⨆ i ∈ s, f (i, i'))
:
(s ×ˢ t).PairwiseDisjoint 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_2}
{ι' : Type u_3}
[Order.Frame α]
{s : Set ι}
{t : Set ι'}
{f : ι × ι' → α}
:
(s ×ˢ t).PairwiseDisjoint f ↔ (s.PairwiseDisjoint fun (i : ι) => ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun (i' : ι') => ⨆ i ∈ s, f (i, i')
theorem
Set.biUnion_diff_biUnion_eq
{α : Type u_1}
{ι : Type u_2}
{s t : Set ι}
{f : ι → Set α}
(h : (s ∪ t).PairwiseDisjoint f)
:
noncomputable def
Set.biUnionEqSigmaOfDisjoint
{α : Type u_1}
{ι : Type u_2}
{s : Set ι}
{f : ι → Set α}
(h : s.PairwiseDisjoint f)
:
Equivalence between a disjoint bounded union and a dependent sum.
Instances For
@[simp]
theorem
Set.coe_biUnionEqSigmaOfDisjoint_symm_apply
{α : Type u_5}
{ι : Type u_6}
{s : Set ι}
{f : ι → Set α}
(h : s.PairwiseDisjoint f)
(x : (i : ↑s) × ↑(f ↑i))
:
↑((biUnionEqSigmaOfDisjoint h).symm x) = ↑x.snd
@[simp]
theorem
Set.coe_snd_biUnionEqSigmaOfDisjoint
{α : Type u_5}
{ι : Type u_6}
{s : Set ι}
{f : ι → Set α}
(h : s.PairwiseDisjoint f)
(x : ↑(⋃ i ∈ s, f i))
:
↑((biUnionEqSigmaOfDisjoint h) x).snd = ↑x
theorem
Set.pairwiseDisjoint_iff
{α : Type u_1}
{ι : Type u_2}
{f : ι → Set α}
{s : Set ι}
:
s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j
theorem
Set.pairwiseDisjoint_pair_insert
{α : Type u_1}
{s : Set α}
{a : α}
(ha : a ∉ s)
:
(𝒫 s).PairwiseDisjoint fun (t : Set α) => {t, insert a t}
theorem
Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion
{α : Type u_1}
{ι : Type u_2}
{f : ι → Set α}
{s t : Set ι}
(h₀ : (s ∪ t).PairwiseDisjoint f)
(h₁ : ∀ i ∈ s, (f i).Nonempty)
(h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i)
:
s ⊆ t
theorem
Pairwise.subset_of_biUnion_subset_biUnion
{α : Type u_1}
{ι : Type u_2}
{f : ι → Set α}
{s t : Set ι}
(h₀ : Pairwise (Function.onFun Disjoint f))
(h₁ : ∀ i ∈ s, (f i).Nonempty)
(h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i)
:
s ⊆ t
theorem
Pairwise.biUnion_injective
{α : Type u_1}
{ι : Type u_2}
{f : ι → Set α}
(h₀ : Pairwise (Function.onFun Disjoint f))
(h₁ : ∀ (i : ι), (f i).Nonempty)
:
Function.Injective fun (s : Set ι) => ⋃ i ∈ s, f i
theorem
pairwiseDisjoint_unique
{α : Type u_1}
{ι : Type u_2}
{f : ι → Set α}
{s : Set ι}
{y : α}
(h_disjoint : s.PairwiseDisjoint f)
(hy : y ∈ ⋃ i ∈ s, f i)
:
In a disjoint union we can identify the unique set an element belongs to.