Set.PairwiseDisjoint.biUnion
theorem Set.PairwiseDisjoint.biUnion :
∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : CompleteLattice α] {s : Set ι'} {g : ι' → Set ι}
{f : ι → α},
(s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i) →
(∀ i ∈ s, (g i).PairwiseDisjoint f) → (⋃ i ∈ s, g i).PairwiseDisjoint f
This theorem, `Set.PairwiseDisjoint.biUnion`, is about the bind operation for `Set.PairwiseDisjoint`. The theorem states that given a set `s` of type `ι'`, a function `g` mapping elements of `ι'` to sets of type `ι`, and a function `f` from `ι` to an element of a complete lattice `α`, if the set `s` is pairwise disjoint for the function that maps each `i'` to the supremum over `i` in `g i'` of `f i`, and for all `i` in `s` the set `g i` is pairwise disjoint for `f`, then the union over `i` in `s` of `g i` is pairwise disjoint for `f`. Here, a set is considered pairwise disjoint if every two different elements in the set are disjoint.
More concisely: If a set and its image under a function to sets of pairwise disjoint elements, where the supremum of a function mapping each set element to an element in a complete lattice is used, are pairwise disjoint for the function, then the union of the sets is pairwise disjoint for that function.
|
Set.PairwiseDisjoint.prod_left
theorem Set.PairwiseDisjoint.prod_left :
∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : CompleteLattice α] {s : Set ι} {t : Set ι'}
{f : ι × ι' → α},
(s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) →
(t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')) → (s ×ˢ t).PairwiseDisjoint f
This theorem, named `Set.PairwiseDisjoint.prod_left`, states that for any complete lattice `α` of some type `u_1`, and sets `s` and `t` of types `u_4` and `u_5` respectively, if the suprema of columns formed by function `f` over `s` and `t` are pairwise disjoint, and the suprema of rows formed by the same function are also pairwise disjoint, then all the elements in the cartesian product of `s` and `t` are pairwise disjoint with respect to function `f`. This should not be confused with `Set.PairwiseDisjoint.prod`.
In other words, pairwise disjointness of the suprema of both rows and columns implies that every pair of elements from the cartesian product of the two sets will be disjoint when evaluated through function `f`.
More concisely: If the suprema of the function evaluations over the columns and rows of two sets are pairwise disjoint in a complete lattice, then every pair of elements from the cartesian product of the sets is disjoint when evaluated through that function.
|