exists_supIrred_decomposition
theorem exists_supIrred_decomposition :
∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : WellFoundedLT α] (a : α),
∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
The theorem `exists_supIrred_decomposition` states that in a well-founded semilattice with a designated bottom element, any given element can be expressed as the supremum of finitely many sup-irreducible elements. A sup-irreducible element, in this context, is defined as a non-bottom element that cannot be the supremum of any smaller elements. This theorem has an analogy in order theory with the prime factorization in number theory, where any number can be expressed as a product of prime numbers.
More concisely: In a well-founded semilattice with a bottom element, every element is the supremum of some finite set of sup-irreducible elements.
|
exists_infIrred_decomposition
theorem exists_infIrred_decomposition :
∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : WellFoundedGT α] (a : α),
∃ s, s.inf id = a ∧ ∀ ⦃b : α⦄, b ∈ s → InfIrred b
The theorem `exists_infIrred_decomposition` states that, for any given type `α` that has a semilattice structure, has a top element, and whose greater-than relation is well-founded, every element `a` of this type can be represented as the infimum (greatest lower bound) of a certain set of finitely many inf-irreducible elements. An inf-irreducible element is a non-top element that is not the infimum of any larger elements. This theorem is an order-theoretic analogue of the prime factorisation in number theory, where every number can be expressed uniquely as a product of prime numbers.
More concisely: Given a semilattice type `α` with top element and well-founded greater-than relation, every element `a` admits a representation as the infimum of a finite set of inf-irreducible elements.
|
InfIrred.ofDual
theorem InfIrred.ofDual :
∀ {α : Type u_2} [inst : SemilatticeSup α] {a : αᵒᵈ}, InfIrred a → SupIrred (OrderDual.ofDual a)
The theorem `InfIrred.ofDual` states that for any type `α` which is an instance of a semilattice with supremum, and for any element `a` of the dual order of `α`, if `a` is an inf-irreducible element (meaning it is not the infimum of any larger elements), then the element in the original order corresponding to `a` (obtained by applying the function `OrderDual.ofDual`) is a sup-irreducible element (meaning it is not the supremum of any smaller elements).
More concisely: If `α` is a semilattice with supremum and `a` is an inf-irreducible element in the dual order of `α`, then `OrderDual.ofDual a` is a sup-irreducible element in `α`.
|
InfIrred.dual
theorem InfIrred.dual :
∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, InfIrred a → SupIrred (OrderDual.toDual a)
The theorem `InfIrred.dual` states that for any type `α` that is an instance of a semilattice with infimum operation (`SemilatticeInf α`), and for any element `a` of `α`, if `a` is an inf-irreducible element (`InfIrred a`), then `a` is also a sup-irreducible element (`SupIrred a`) in the order dual (`OrderDual.toDual a`) of `α`. In simpler terms, if an element is inf-irreducible in a semilattice, then it is sup-irreducible in the order dual of that semilattice.
More concisely: If `α` is a semilattice with infimum and `a` is an inf-irreducible element, then `a` is sup-irreducible in the dual order of `α`.
|
SupIrred.supPrime
theorem SupIrred.supPrime : ∀ {α : Type u_2} [inst : DistribLattice α] {a : α}, SupIrred a → SupPrime a
The theorem named `SupIrred.supPrime` asserts that for any type `α` that forms a distributive lattice and any element `a` of type `α`, if `a` is a supremum-irreducible element, then `a` is also a supremum-prime element. In other words, if `a` is an element that is not the least element and isn't the supremum of any two smaller elements, then `a` is also an element that is not the least and isn't less than the supremum of any two smaller elements.
More concisely: If `α` is a distributive lattice and `a` is a supremum-irreducible element in `α`, then `a` is a supremum-prime element.
|
InfPrime.ofDual
theorem InfPrime.ofDual :
∀ {α : Type u_2} [inst : SemilatticeSup α] {a : αᵒᵈ}, InfPrime a → SupPrime (OrderDual.ofDual a)
The theorem `InfPrime.ofDual` states that for any type `α` that has a semilattice structure with supremum, if an element `a` of the dual order of `α` is an infimum-prime element, then the same element `a` under the identity function `OrderDual.ofDual` is a supremum-prime element in `α`. In other words, it shows a correspondence between infimum-prime elements in the dual order and supremum-prime elements in the original order.
More concisely: If `α` is a type with a semilattice structure and supremum, and `a` is an infimum-prime element in the dual order of `α`, then `OrderDual.ofDual a` is a supremum-prime element in `α`.
|
SupPrime.dual
theorem SupPrime.dual :
∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, SupPrime a → InfPrime (OrderDual.toDual a)
This theorem states that for any type `α` with a Sup-semilattice structure and any element `a` of that type, if `a` is a supremum-prime element, then the dual of `a` is an infimum-prime element under the dual order. Here, a supremum-prime element is a non-minimal element that is not less than the supremum of any pair of smaller elements, and an infimum-prime element is a non-maximal element that is not greater than the infimum of any pair of larger elements. The `OrderDual.toDual a` function simply gives the dual order of `a`.
More concisely: For any type `α` with a Sup-semilattice structure and any supremum-prime element `a`, the dual of `a` is an infimum-prime element under the dual order.
|
SupIrred.ofDual
theorem SupIrred.ofDual :
∀ {α : Type u_2} [inst : SemilatticeInf α] {a : αᵒᵈ}, SupIrred a → InfIrred (OrderDual.ofDual a)
The theorem `SupIrred.ofDual` states that for any type `α` which is a semilattice with infimum, and for any object `a` of the dual type of `α`, if `a` is supremum-irreducible, then the image of `a` under the identity function from the dual of `α` to `α` is infimum-irreducible. In other words, a supremum-irreducible element in a dual order becomes an infimum-irreducible element when we consider it in the original order.
More concisely: If `α` is a semilattice with infimum and `a` is a supremum-irreducible element in the dual order of `α`, then the image of `a` under the identity function is infimum-irreducible in `α`.
|
InfPrime.dual
theorem InfPrime.dual :
∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, InfPrime a → SupPrime (OrderDual.toDual a)
The theorem `InfPrime.dual` states that for any type `α` that is a semilattice with respect to the infimum operation, and for any element `a` of type `α`, if `a` is an inf-prime element (i.e., it is not the maximum element and it is not greater than the infimum of any other two elements `b` and `c`), then the dual of `a` (which is just `a` itself because `OrderDual.toDual` is the identity function) is a sup-prime element in the dual order (i.e., it is not the minimum element and it is not less than the supremum of any other two elements `b` and `c`). This theorem is essentially establishing the duality between inf-prime and sup-prime elements in a semilattice.
More concisely: In a semilattice, if an element is inf-prime (not maximum and not below the infimum of any two elements), then its dual is sup-prime (not minimum and not above the supremum of any two elements).
|
SupPrime.ofDual
theorem SupPrime.ofDual :
∀ {α : Type u_2} [inst : SemilatticeInf α] {a : αᵒᵈ}, SupPrime a → InfPrime (OrderDual.ofDual a)
The theorem `SupPrime.ofDual` states that for any type `α` that is a semilattice with an infimum operation, and for any element `a` of the dual order of `α`, if `a` is a supremum-prime element, then the element of `α` that corresponds to `a` under the identity function from the dual order to the original order (`OrderDual.ofDual a`) is an infimum-prime element. In other words, it converts supremum-prime elements in the dual order of a lattice into infimum-prime elements in the original lattice.
More concisely: For any semilattice `α` with an infimum operation and any supremum-prime element `a` in its dual order, `OrderDual.ofDual a` is an infimum-prime element in `α`.
|
SupIrred.dual
theorem SupIrred.dual :
∀ {α : Type u_2} [inst : SemilatticeSup α] {a : α}, SupIrred a → InfIrred (OrderDual.toDual a)
This theorem, referred to as "SupIrred.dual", states that for any type `α` that has a `SemilatticeSup` structure, and for any element `a` of `α`, if `a` is a supremum-irreducible element, then the dual of `a` (i.e., `OrderDual.toDual a`) is an infimum-irreducible element. In other words, if an element is such that it's not the least element and not the supremum of any two smaller elements, then its dual will be such that it's not the greatest element and not the infimum of any two larger elements.
More concisely: If `α` is a type with a `SemilatticeSup` structure and `a` is a supremum-irreducible element, then the dual of `a` is an infimum-irreducible element.
|
InfIrred.infPrime
theorem InfIrred.infPrime : ∀ {α : Type u_2} [inst : DistribLattice α] {a : α}, InfIrred a → InfPrime a
The theorem `InfIrred.infPrime` states that for any type `α` that forms a distributive lattice, if an element `a` of type `α` is inf-irreducible, then it is also inf-prime. In the context of lattices, an inf-irreducible element is a non-top element which isn't the infimum of anything larger, and an inf-prime element is a non-top element which isn't larger than the infimum of anything larger. This theorem shows the one-way implication from being inf-irreducible to being inf-prime.
More concisely: If `α` is a distributive lattice and `a` is an inf-irreducible element in `α`, then `a` is inf-prime.
|