Documentation

Mathlib.Data.Set.Pairwise.Lattice

Relations holding pairwise #

In this file we prove many facts about Pairwise and the set lattice.

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 as, 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 sSet.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 : is, 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')) :

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')
theorem Set.biUnion_diff_biUnion_eq {α : Type u_1} {ι : Type u_4} {s : Set ι} {t : Set ι} {f : ιSet α} (h : Set.PairwiseDisjoint (s t) f) :
(⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f 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
  • One or more equations did not get rendered due to their size.
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₁ : is, Set.Nonempty (f i)) (h : ⋃ i ∈ s, f i ⋃ i ∈ t, f i) :
    s t
    theorem Pairwise.subset_of_biUnion_subset_biUnion {α : Type u_1} {ι : Type u_4} {f : ιSet α} {s : Set ι} {t : Set ι} (h₀ : Pairwise (Disjoint on f)) (h₁ : is, 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