mathlib3 documentation

data.set.pairwise.lattice

Relations holding pairwise #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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
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
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
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) :
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.

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'))) :

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.

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'))
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
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
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
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
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)