Finset.SupIndep.pairwiseDisjoint
theorem Finset.SupIndep.pairwiseDisjoint :
∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
s.SupIndep f → (↑s).PairwiseDisjoint f
The theorem `Finset.SupIndep.pairwiseDisjoint` states that for any set `s` of elements of type `ι` and any function `f` from `ι` to `α`, where `α` is a lattice and an ordered bot (it contains a least element), if `s` enjoys the supremum independence property under `f`, then the set `s` (viewed as a set instead of a finset) is pairwise disjoint under `f`. In other words, the images of any two distinct elements of `s` under `f` are disjoint. Supremum independence implies that for any subset `t` of `s` and any element `i` in `s` but not in `t`, `f(i)` is disjoint from the supremum of `f` over `t`.
More concisely: If a set `s` of elements from a lattice `α` with a least element has the supremum independence property under a function `f` from `s` to `α`, then the images of distinct elements of `s` under `f` are disjoint.
|
Finset.sup_indep.pairwise_disjoint
theorem Finset.sup_indep.pairwise_disjoint :
∀ {α : Type u_1} {ι : Type u_3} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
s.SupIndep f → (↑s).PairwiseDisjoint f
This theorem, `Finset.sup_indep.pairwise_disjoint`, is an alias for the forward direction of another theorem, `Finset.supIndep_iff_pairwiseDisjoint`. It defines that for any types `α` and `ι`, any distributed lattice and ordered bottom structure over `α`, a finite set `s` of type `ι`, and a function `f` from `ι` to `α`, if the supremum of `s` under `f` is independent, then the elements of `s` are pairwise disjoint under `f`. This means that if the supremum of the elements in the set doesn't depend on any particular element, then no two elements in the set have the same image under the function `f`.
More concisely: If a finite set and a function have an independent supremum, then the elements of the set are pairwise disjoint in the image of the function.
|
CompleteLattice.Independent.sup_indep_univ
theorem CompleteLattice.Independent.sup_indep_univ :
∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [inst_1 : Fintype ι] {f : ι → α},
CompleteLattice.Independent f → Finset.univ.SupIndep f
The theorem `CompleteLattice.Independent.sup_indep_univ` is an alias of the forward direction of `CompleteLattice.independent_iff_supIndep_univ`. This theorem states that for any type `α` that forms a complete lattice, and any finitely enumerable index type `ι`, if `f` is a function from `ι` to `α` that satisfies the property of lattice independence, then `f` is supremum-independent over the universal finset `univ` of `ι` (i.e., every element of `α` produced by `f` is independent of the supremum of any subset of other elements).
More concisely: For any complete lattice `α` and finitely enumerable index type `ι`, if `f : ι → α` satisfies lattice independence, then `f` is supremum-independent over the universal set `univ` of `ι`.
|
Finset.SupIndep.biUnion
theorem Finset.SupIndep.biUnion :
∀ {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : DistribLattice α] [inst_1 : OrderBot α]
[inst_2 : DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
(s.SupIndep fun i => (g i).sup f) → (∀ i' ∈ s, (g i').SupIndep f) → (s.biUnion g).SupIndep f
The theorem `Finset.SupIndep.biUnion` states that for any types `α`, `ι`, and `ι'`, and given a distributive lattice structure on `α`, a bottom element for `α`, and a decidable equality on `ι`, if we have a finite set `s` of type `ι'`, a function `g` mapping elements of `ι'` to finite sets of `ι`, and a function `f` mapping elements of `ι` to `α`, then if `s` is supremum-independent with respect to the supremum of `f` over the images of `g`, and for every element `i'` in `s`, the image of `i'` under `g` is supremum-independent with respect to `f`, then the binary union of `s` and `g` is supremum-independent with respect to `f`. In simpler words, the supremum-independence property is preserved under the binary union operation.
More concisely: If `s` is a supremum-independent set with respect to the supremum of `f` over the images of `g` for a distributive lattice `α` with bottom element, decidable equality on index types `ι` and `ι'`, and functions `f : ι -> α` and `g : ι' -> Fin ι`, then the binary union of `s` and the images of `s` under `g` is supremum-independent with respect to `f`.
|
CompleteLattice.Independent.disjoint_biSup
theorem CompleteLattice.Independent.disjoint_biSup :
∀ {ι : Type u_5} {α : Type u_6} [inst : CompleteLattice α] {t : ι → α},
CompleteLattice.Independent t → ∀ {x : ι} {y : Set ι}, x ∉ y → Disjoint (t x) (⨆ i ∈ y, t i)
This theorem states that in a complete lattice, if the elements are independent, then any given element is disjoint from the supremum of any subset of the remaining elements. Here, an element is considered independent if it is not dependent on or influenced by the others. Disjoint, in this context, means that the infimum of two elements of the lattice is the bottom element of the lattice. The supremum (denoted by `⨆`) of a set of elements is the least element that is greater than or equal to every element of the set.
More concisely: In a complete lattice, if elements are independent, then each element is disjoint from the supremum of any subset of the other elements.
|
CompleteLattice.Independent.pairwiseDisjoint
theorem CompleteLattice.Independent.pairwiseDisjoint :
∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α},
CompleteLattice.Independent t → Pairwise (Disjoint on t)
This theorem states that if the elements of a set are independent in a complete lattice, then any pair of elements within that set is disjoint. Specifically, for any type α that forms a complete lattice and any function `t` from some index set ι to α, if the elements of the function's range are independent (meaning no element is below the join of some other elements), then any two distinct elements in the range of `t` are disjoint. Here, two elements `a` and `b` are considered disjoint if any element `x` that is below both `a` and `b` must also be below the bottom ('⊥') element of the lattice.
More concisely: In a complete lattice, if the elements of a function from an index set to the lattice are independent, then any two distinct elements in the range are disjoint.
|
CompleteLattice.independent_map_orderIso_iff
theorem CompleteLattice.independent_map_orderIso_iff :
∀ {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β)
{a : ι → α}, CompleteLattice.Independent (⇑f ∘ a) ↔ CompleteLattice.Independent a
This theorem states that for any sort `ι`, types `α` and `β` with both having a CompleteLattice instance, and a function `f` that is an order isomorphism between `α` and `β`, the function `a` from `ι` to `α` is independent (in the sense of complete lattices) if and only if the function `f ∘ a` (i.e., the composition of `f` and `a`) is independent. In other words, independence of a function in the domain of the order isomorphism is preserved under the mapping of the order isomorphism.
More concisely: For any order isomorphism `f` between complete lattices `α` and `β`, and any independent function `a` from a sort `ι` to `α`, the function `f ∘ a` is also independent in `β`.
|
Set.PairwiseDisjoint.supIndep
theorem Set.PairwiseDisjoint.supIndep :
∀ {α : Type u_1} {ι : Type u_3} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
(↑s).PairwiseDisjoint f → s.SupIndep f
This theorem, `Set.PairwiseDisjoint.supIndep`, states that given a finite set `s` and a function `f` from elements of `s` to some type `α` (where `α` forms a distributive lattice and has a least element), if the set `s` is pairwise disjoint with respect to `f`, then `s` is supremum-independent with respect to `f`. In this context, a set is pairwise disjoint if, for any two distinct elements in the set, the function `f` returns different values. Similarly, a set is supremum-independent if the supremum of the function `f` over any subset of `s` does not equal the function `f` applied to any element of the subset.
More concisely: Given a finite set endowed with a distributive lattice and a least element, if the elements of the set are pairwise mapped to distinct values under a function, then the set is supremum-independent with respect to that function.
|
CompleteLattice.Independent.comp
theorem CompleteLattice.Independent.comp :
∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ι → α} {f : ι' → ι},
CompleteLattice.Independent t → Function.Injective f → CompleteLattice.Independent (t ∘ f)
The theorem `CompleteLattice.Independent.comp` states that for all types `α` with a complete lattice structure, given any indexed family `t : ι → α`, and any injective function `f : ι' → ι`, if the indexed family `t` is independent, then the composition of `t` and `f`, denoted as `t ∘ f`, also forms an independent indexed family. In other words, composing an independent indexed family with an injective function on the index results in another independent indexed family.
More concisely: For any complete lattice type `α` and injective function `f`, if `t : ι → α` is an independent indexed family, then `t ∘ f : ι' → α` is also an independent indexed family.
|
CompleteLattice.independent_iff_supIndep_univ
theorem CompleteLattice.independent_iff_supIndep_univ :
∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [inst_1 : Fintype ι] {f : ι → α},
CompleteLattice.Independent f ↔ Finset.univ.SupIndep f
This theorem provides a variant of `CompleteLattice.independent_iff_supIndep` specifically for finite types (`Fintype`s). Specifically, for any types `α` and `ι`, given that `α` is a complete lattice and `ι` is a finite type, and any function `f` from `ι` to `α`, it states that `f` being independent in the complete lattice structure is equivalent to `f` being supremum independent over the universal finite set of `ι`. In terms of lattice theory, this equivalence bridges the notion of independence in a complete lattice and supremum independence in a finite set context.
More concisely: For a complete lattice `α` and finite type `ι`, the function `f` from `ι` to `α` is independent in `α` if and only if it is supremum independent over the universal set of `ι`.
|
Finset.SupIndep.sup
theorem Finset.SupIndep.sup :
∀ {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [inst : DistribLattice α] [inst_1 : OrderBot α]
[inst_2 : DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α},
(s.SupIndep fun i => (g i).sup f) → (∀ i' ∈ s, (g i').SupIndep f) → (s.sup g).SupIndep f
This theorem states that for any types `α`, `ι`, `ι'`, where `α` has a distributive lattice structure and a least element (`OrderBot`), and `ι` has decidable equality (`DecidableEq`), given a finite set `s` of type `ι'`, a function `g` mapping `ι'` to a finite set of type `ι`, and a function `f` mapping `ι` to `α`, if the supremum of the sets `g i` (for `i` in `s`) with respect to `f` is independent (`SupIndep`), and for each element `i'` in `s`, the set `g i'` is also `SupIndep` with respect to `f`, then the supremum of the set `s` with respect to `g` is `SupIndep` with respect to `f`.
In simpler terms, this theorem establishes a condition under which the supremum of a set of sets remains independent when the sets themselves are independent.
More concisely: If `α` is a distributive lattice with least element, `ι` has decidable equality, `s` is a finite set of `ι'`, `g` maps `ι'` to finite subsets of `ι`, `f` maps `ι` to `α`, and for all `i` in `s`, the sets `g i` and the supremum of `g i` with respect to `f` are independent, then the supremum of `s` with respect to `g` is independent with respect to `f`.
|
Mathlib.Order.SupIndep._auxLemma.25
theorem Mathlib.Order.SupIndep._auxLemma.25 :
∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
[inst_2 : DecidableEq ι], s.SupIndep f = ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
This theorem states that for any types `α` and `ι`, given a lattice structure and a bottom element for `α`, a finite set `s` of type `ι`, and a function `f` mapping `ι` to `α`, if we have decidable equality for `ι`, then `s` is supremum independent with respect to `f` if and only if for every element `i` in `s`, `f(i)` is disjoint with the supremum of the set obtained by applying `f` to each element of `s` after erasing `i`. Here, two elements `a` and `b` are said to be disjoint if for any `x` that is lesser than or equal to both `a` and `b`, `x` is also less than or equal to the bottom element. The supremum of a finite set is the maximum value obtained by applying `f` to each element of the set.
More concisely: For any lattice with a bottom element, a function from a finite set to the lattice, and decidable equality, a set is supremum independent if and only if the image of each element under the function is disjoint with the supremum of the images of all elements after removing that element.
|
CompleteLattice.Independent.map_orderIso
theorem CompleteLattice.Independent.map_orderIso :
∀ {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β)
{a : ι → α}, CompleteLattice.Independent a → CompleteLattice.Independent (⇑f ∘ a)
This theorem states that if we have an independent indexed family in a complete lattice, then after applying an order isomorphism to each element of the family, the resulting family will still be independent. More specifically, for any sort `ι`, types `α` and `β`, and given that `α` and `β` are complete lattices, if `f` is an order isomorphism from `α` to `β` and `a` is an independent function from `ι` to `α`, then the composition of `f` and `a` yields another independent function.
More concisely: If `α` and `β` are complete lattices, `f` is an order isomorphism from `α` to `β`, and `a` is an independent function from an indexing type `ι` to `α`, then the composition of `f` and `a` is an independent function from `ι` to `β`.
|
Set.PairwiseDisjoint.setIndependent
theorem Set.PairwiseDisjoint.setIndependent :
∀ {α : Type u_1} [inst : Order.Frame α] {s : Set α}, s.PairwiseDisjoint id → CompleteLattice.SetIndependent s := by
sorry
The theorem `Set.PairwiseDisjoint.setIndependent` states that for any set `s` within a type `α` that has an `Order.Frame` structure, if `s` is pairwise disjoint (i.e., every pair of distinct elements in `s` are disjoint), then `s` is an independent set in the complete lattice sense. In other words, for every element `a` in `s`, it is disjoint from the supremum of the other elements in `s`.
More concisely: If a set in an order frame is pairwise disjoint, then each of its elements is disjoint from the supremum of the other elements in the set.
|
Finset.SupIndep.sigma
theorem Finset.SupIndep.sigma :
∀ {α : Type u_1} {ι : Type u_3} [inst : DistribLattice α] [inst_1 : OrderBot α] {β : ι → Type u_5} {s : Finset ι}
{g : (i : ι) → Finset (β i)} {f : Sigma β → α},
(s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩) →
(∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩) → (s.sigma g).SupIndep f
The theorem `Finset.SupIndep.sigma` states that for any types `α`, `ι`, and any function `β` from `ι` to some type, along with a distributive lattice structure on `α` and a minimal element (`OrderBot`), if we have a finite set `s` of type `ι`, a function `g` mapping each element of `ι` to a finite set of the corresponding type `β i`, and a function `f` from the sigma type `Sigma β` to `α`, then if the supremum of the set resulting from applying `f` to each element of the product of `s` and `g i` (for each `i` in `s`) is independent of the order of the elements, and the supremum of the set resulting from applying `f` to each element of `g i` is also independent of the order for all `i` in `s`, then the supremum of the set resulting from applying `f` to each element of the sigma type of `s` and `g` is likewise independent of the order of the elements.
More concisely: If `f` maps a finite set of functions from `ι` to a distributive lattice with minimal element to a common supremum independently of the order of elements, and the supremum of each function is also order-independent, then the supremum of `f` over the sigma type of these functions is order-independent as well.
|
CompleteLattice.SetIndependent.disjoint_sSup
theorem CompleteLattice.SetIndependent.disjoint_sSup :
∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α},
CompleteLattice.SetIndependent s → ∀ {x : α} {y : Set α}, x ∈ s → y ⊆ s → x ∉ y → Disjoint x (sSup y)
The theorem states that in a complete lattice, if a set of elements is independent, then any particular element of the set is disjoint from the supremum of any subset of the remaining elements. In this context, a set of elements in a lattice is called independent if every element is disjoint from the supremum of the rest of the set. Two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element of the lattice. The theorem articulates a property of independent sets in complete lattices where the supremum (least upper bound) of a subset doesn't interfere with any element not in the subset.
More concisely: In a complete lattice, an independent set of elements has each element disjoint from the supremum of any subset of the remaining elements.
|
Finset.SupIndep.independent_of_univ
theorem Finset.SupIndep.independent_of_univ :
∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [inst_1 : Fintype ι] {f : ι → α},
Finset.univ.SupIndep f → CompleteLattice.Independent f
The theorem `Finset.SupIndep.independent_of_univ` states that for any type `α` that forms a complete lattice, any `Fintype` ι, and any function `f` mapping from ι to α, if `f` is supremum-independent over the universal set of ι (`Finset.univ.SupIndep f`), then `f` is also independent in the complete lattice sense (`CompleteLattice.Independent f`). This theorem is essentially a specific version of `CompleteLattice.independent_iff_supIndep` for `Fintype`s, and serves as an alias for the reverse direction of `CompleteLattice.independent_iff_supIndep_univ`.
More concisely: For any complete lattice α and Fintype ι, if a function from ι to α is supremum-independent over the universal set, then it is independent in the complete lattice.
|
CompleteLattice.Independent.supIndep
theorem CompleteLattice.Independent.supIndep :
∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {s : Finset ι} {f : ι → α},
CompleteLattice.Independent (f ∘ Subtype.val) → s.SupIndep f
The theorem `CompleteLattice.Independent.supIndep` states that for any types `α` and `ι`, where `α` is a complete lattice, a given finset `s` of type `ι`, and a function `f : ι → α`, if the composition of `f` with the `Subtype.val` function is independent (in the sense of `CompleteLattice.Independent`), then `s` is supremum-independent under `f` (denoted as `s.SupIndep f`). In other words, if each element's image under `f` doesn't depend on the others, then the supremum of any subset of `s` under `f` equals the supremum of their images under `f`.
More concisely: If `f : ι → α` is a function from a set `ι` to a complete lattice `α`, and the images of distinct elements under `f` are independent, then any subset of `ι` is supremum-independent under `f`.
|
Finset.SupIndep.independent
theorem Finset.SupIndep.independent :
∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {s : Finset ι} {f : ι → α},
s.SupIndep f → CompleteLattice.Independent (f ∘ Subtype.val)
This theorem states that for any types `α` and `ι`, provided `α` is a complete lattice, and for any finite set `s` of type `ι` and function `f` from `ι` to `α`, if `s` is supremum-independent with respect to `f`, then the function `f` composed with the underlying value function of a subtype is independent in the sense of `CompleteLattice.Independent`. In terms of lattice theory, this means that the elements of the image of the function are pairwise disjoint in the lattice.
More concisely: For any complete lattice `α` and function `f` from a finite, supremum-independent set `s` of type `ι` to `α`, the images of distinct elements of `s` under `f` are lattice-disjoint.
|
CompleteLattice.SetIndependent.pairwiseDisjoint
theorem CompleteLattice.SetIndependent.pairwiseDisjoint :
∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, CompleteLattice.SetIndependent s → s.PairwiseDisjoint id
The theorem states that if a set of elements in a complete lattice is independent, meaning that each element is disjoint from the supremum of the rest of the set, then any pair of elements within that set are also disjoint. In other words, if the independence condition specified by `CompleteLattice.SetIndependent` is satisfied by a set `s` in a complete lattice `α`, then the property `s.PairwiseDisjoint id` is necessarily true, which asserts that for any two distinct elements in the set, we have that the elements are disjoint.
More concisely: In a complete lattice, if a set of elements is independent, then any two distinct elements in the set are disjoint.
|
Finset.supIndep_iff_disjoint_erase
theorem Finset.supIndep_iff_disjoint_erase :
∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
[inst_2 : DecidableEq ι], s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
This theorem states that for any type `α` with a lattice structure and a bottom element, and any function `f : ι → α` from some type `ι` to `α`, a finite set `s` of type `ι` is supremum-independent with respect to `f` if and only if, for all elements `i` in `s`, `f(i)` is disjoint with the supremum of `f` over the set `s` obtained by erasing the element `i`. Here, two elements of the lattice are said to be disjoint if their infimum is the bottom element. The property of supremum-independence generalizes the concept of linear independence to lattices. The theorem uses decidability of equality in type `ι`, which means that given any two elements of type `ι`, it's decidable whether they are equal or not.
More concisely: For any lattice type `α` with a bottom element, and a function `f` from a type `ι` to `α`, a finite set `s` of `ι` is supremum-independent with respect to `f` if and for all `i` in `s`, `f(i)` and the supremum of `f(j)` over `j` in `s` without `i` are disjoint.
|
CompleteLattice.SetIndependent.mono
theorem CompleteLattice.SetIndependent.mono :
∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α},
CompleteLattice.SetIndependent s → ∀ {t : Set α}, t ⊆ s → CompleteLattice.SetIndependent t
The theorem `CompleteLattice.SetIndependent.mono` states that for any type `α` that forms a complete lattice, if a set `s` of elements of `α` is independent (meaning every element in `s` is disjoint from the supremum of the remaining elements in `s`), then for any subset `t` of `s`, `t` is also independent. In other words, independence is preserved under taking subsets in a complete lattice.
More concisely: In a complete lattice, any independent subset is closed under subsets.
|