data.set.pairwise.lattice

source

theorem set.pairwise_Union {α : Type u_1} {κ : Sort u_6} {r : α → α → Prop} {f : κ → set α} (h : directed has_subset.subset f) :

(⋃ (n : κ), f n).pairwise r ↔ ∀ (n : κ), (f n).pairwise r

source

theorem set.pairwise_sUnion {α : Type u_1} {r : α → α → Prop} {s : set (set α)} (h : directed_on has_subset.subset s) :

(⋃₀ s).pairwise r ↔ ∀ (a : set α), a ∈ s → a.pairwise r

source

theorem set.pairwise_disjoint_Union {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [partial_order α] [order_bot α] {f : ι → α} {g : ι' → set ι} (h : directed has_subset.subset g) :

(⋃ (n : ι'), g n).pairwise_disjoint f ↔ ∀ ⦃n : ι'⦄, (g n).pairwise_disjoint f

source

theorem set.pairwise_disjoint_sUnion {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {f : ι → α} {s : set (set ι)} (h : directed_on has_subset.subset s) :

(⋃₀ s).pairwise_disjoint f ↔ ∀ ⦃a : set ι⦄, a ∈ s → a.pairwise_disjoint f

source

theorem set.pairwise_disjoint.bUnion {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [complete_lattice α] {s : set ι'} {g : ι' → set ι} {f : ι → α} (hs : s.pairwise_disjoint (λ (i' : ι'), ⨆ (i : ι) (H : i ∈ g i'), f i)) (hg : ∀ (i : ι'), i ∈ s → (g i).pairwise_disjoint f) :

(⋃ (i : ι') (H : i ∈ s), g i).pairwise_disjoint f

Bind operation for set.pairwise_disjoint. If you want to only consider finsets of indices, you can use set.pairwise_disjoint.bUnion_finset.

source

theorem set.pairwise_disjoint.prod_left {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [complete_lattice α] {s : set ι} {t : set ι'} {f : ι × ι' → α} (hs : s.pairwise_disjoint (λ (i : ι), ⨆ (i' : ι') (H : i' ∈ t), f (i, i'))) (ht : t.pairwise_disjoint (λ (i' : ι'), ⨆ (i : ι) (H : i ∈ s), f (i, i'))) :

(s ×ˢ t).pairwise_disjoint 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.pairwise_disjoint.prod.

source

theorem set.pairwise_disjoint_prod_left {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [order.frame α] {s : set ι} {t : set ι'} {f : ι × ι' → α} :

(s ×ˢ t).pairwise_disjoint f ↔ s.pairwise_disjoint (λ (i : ι), ⨆ (i' : ι') (H : i' ∈ t), f (i, i')) ∧ t.pairwise_disjoint (λ (i' : ι'), ⨆ (i : ι) (H : i ∈ s), f (i, i'))

source

theorem set.bUnion_diff_bUnion_eq {α : Type u_1} {ι : Type u_4} {s t : set ι} {f : ι → set α} (h : (s ∪ t).pairwise_disjoint f) :

((⋃ (i : ι) (H : i ∈ s), f i) \ ⋃ (i : ι) (H : i ∈ t), f i) = ⋃ (i : ι) (H : i ∈ s \ t), f i

source

noncomputable def set.bUnion_eq_sigma_of_disjoint {α : Type u_1} {ι : Type u_4} {s : set ι} {f : ι → set α} (h : s.pairwise_disjoint f) :

(↥⋃ (i : ι) (H : i ∈ s), f i) ≃ Σ (i : ↥s), ↥(f ↑i)

Equivalence between a disjoint bounded union and a dependent sum.

Equations

set.bUnion_eq_sigma_of_disjoint h = (equiv.set_congr set.bUnion_eq_sigma_of_disjoint._proof_1).trans (set.Union_eq_sigma_of_disjoint _)

source

theorem set.pairwise_disjoint.subset_of_bUnion_subset_bUnion {α : Type u_1} {ι : Type u_4} {f : ι → set α} {s t : set ι} (h₀ : (s ∪ t).pairwise_disjoint f) (h₁ : ∀ (i : ι), i ∈ s → (f i).nonempty) (h : (⋃ (i : ι) (H : i ∈ s), f i) ⊆ ⋃ (i : ι) (H : i ∈ t), f i) :

s ⊆ t

source

theorem pairwise.subset_of_bUnion_subset_bUnion {α : Type u_1} {ι : Type u_4} {f : ι → set α} {s t : set ι} (h₀ : pairwise (disjoint on f)) (h₁ : ∀ (i : ι), i ∈ s → (f i).nonempty) (h : (⋃ (i : ι) (H : i ∈ s), f i) ⊆ ⋃ (i : ι) (H : i ∈ t), f i) :

s ⊆ t

source

theorem pairwise.bUnion_injective {α : Type u_1} {ι : Type u_4} {f : ι → set α} (h₀ : pairwise (disjoint on f)) (h₁ : ∀ (i : ι), (f i).nonempty) :

function.injective (λ (s : set ι), ⋃ (i : ι) (H : i ∈ s), f i)

mathlib3 documentation

Relations holding pairwise #