disjoint_bot_right
theorem disjoint_bot_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a ⊥ := by
sorry
The theorem `disjoint_bot_right` states that for any type `α` that has a partial order and a least element (denoted as `⊥`), any element `a` of this type is disjoint with the least element `⊥`. In the context of lattices, two elements are considered disjoint if their greatest lower bound (infimum) is the bottom element. Hence, in this case, if `a` and `⊥` are elements of type `α`, then they are disjoint because their greatest lower bound cannot be anything other than `⊥`.
More concisely: For any type `α` with a partial order and least element `⊥`, `a` and `⊥` are disjoint in the sense that their greatest lower bound is `⊥` for all `a` in `α`.
|
ComplementedLattice.exists_isCompl
theorem ComplementedLattice.exists_isCompl :
∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [self : ComplementedLattice α] (a : α),
∃ b, IsCompl a b
This theorem states that in a complimented lattice, each element has a complement. Specifically, for every type `α` that has a structure of a lattice, a bounded order, and is a complemented lattice, there exists an element `b` such that `b` is the complement of any given element `a` in the lattice. In mathematical terms, a complemented lattice is a bounded lattice (with least element 0 and greatest element 1), in which every element `a` has a complement `b` such that the meet (`a ∧ b`) is the least element (0) and the join (`a ∨ b`) is the greatest element (1).
More concisely: In a complemented lattice, every element has a complement such that the meet of the element with its complement is the least element, and the join is the greatest element.
|
codisjoint_iff_le_sup
theorem codisjoint_iff_le_sup :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b ↔ ⊤ ≤ a ⊔ b
The theorem `codisjoint_iff_le_sup` states that for any type `α` with an order structure that is both a semilattice with respect to the operation 'sup' (denoted by ⊔) and has a top element (denoted by ⊤), and for any two elements `a` and `b` of this type, `a` and `b` are codisjoint if and only if the top element (⊤) is less than or equal to the supremum of `a` and `b` (denoted by a ⊔ b). Here, 'codisjoint' means that for any element `x` in the order, if `a` and `b` are both less than or equal to `x`, then the top element is less than or equal to `x`.
More concisely: For any semilattice with top element order structure type α, elements a and b are codisjoint if and only if ⊤ ≤ a ⊔ b.
|
Disjoint.mono
theorem Disjoint.mono :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c d : α},
a ≤ b → c ≤ d → Disjoint b d → Disjoint a c
The theorem `Disjoint.mono` states that for any type `α` that is a partial order and has a bottom element (`OrderBot α`), given four elements `a`, `b`, `c`, `d` of `α`, if `a` is less than or equal to `b` and `c` is less than or equal to `d`, and if `b` and `d` are disjoint (i.e., their greatest lower bound is the bottom element of the order), then `a` and `c` are also disjoint. This is a monotonicity property of the notion of disjointness in lattices.
More concisely: If `α` is a partial order with bottom element, `a` and `b`, and `c` and `d` in `α` are such that `a ≤ b`, `c ≤ d`, and `b` and `d` are disjoint, then `a` and `c` are disjoint.
|
Codisjoint_comm
theorem Codisjoint_comm :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b ↔ Codisjoint b a := by
sorry
The theorem `Codisjoint_comm` states that for any two elements `a` and `b` of a type `α` that has a partial order and a top element, `a` and `b` are codisjoint if and only if `b` and `a` are codisjoint. In other words, the property of being codisjoint is commutative. Recall that in this context, two elements `a` and `b` are said to be codisjoint if for any element `x` of `α` such that `a` and `b` are both less than or equal to `x`, then the top element of `α` is also less than or equal to `x`.
More concisely: For any partial order with top element, elements `a` and `b` are codisjoint if and only if `b` and `a` are codisjoint. (i.e. the property of being codisjoint is commutative.)
|
Mathlib.Order.Disjoint._auxLemma.4
theorem Mathlib.Order.Disjoint._auxLemma.4 :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a a = (a = ⊥)
The theorem, `Mathlib.Order.Disjoint._auxLemma.4`, states that for any type `α` that has a partial order and a least element (denoted by `⊥`), an element `a` of `α` is said to be disjoint with itself if and only if `a` is the bottom element `⊥`. This is a property of lattice theory, where the term "disjoint" is generalized to mean that the infimum (greatest lower bound) of two elements is the bottom element. In this case, the theorem deals with the special scenario where the two elements are identical.
More concisely: For any type `α` with a partial order and a least element `⊥`, an element `a` is disjoint with itself if and only if `a = ⊥`.
|
disjoint_iff
theorem disjoint_iff :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b = ⊥
This theorem states that for any type `α` that is a semilattice (an algebraic structure with a binary operation that is associative, commutative, and idempotent, and also has a partial order relation that is compatible with the binary operation) with the infimum operation and a least element (denoted as ⊥), and for any two elements `a` and `b` of this type, `a` and `b` are disjoint if and only if their infimum (the greatest lower bound) is the least element (⊥). In simple terms, two elements are disjoint if their greatest common lower bound is the smallest possible element in the set.
More concisely: For any semilattice with infimum and least element, two elements are disjoint if and only if their infimum equals the least element.
|
Disjoint.ne
theorem Disjoint.ne :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, a ≠ ⊥ → Disjoint a b → a ≠ b
This theorem states that for any type `α` that has a partial order and a bottom element, if two elements `a` and `b` of `α` are disjoint, and `a` is not the bottom element, then `a` and `b` cannot be equal. In other words, if `a` is disjoint from `b` and `a` is not the least element of the partial order, then `a` is necessarily different from `b`. The concept of disjointness here generalizes the idea of disjoint sets: in a lattice structure, two elements are considered disjoint if their greatest lower bound (infimum) is the bottom element of the lattice.
More concisely: For any type `α` with a bottom element and a partial order, if `a` and `b` are disjoint elements of `α` and `a` is not the bottom element, then `a` is distinct from `b`.
|
disjoint_right_comm
theorem disjoint_right_comm :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b c : α},
Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b
This theorem states that for any semilattice (a partially ordered set in which any two elements have a greatest lower bound) of type `α` with a minimum element (`OrderBot α`), and any three elements `a`, `b`, and `c` of `α`, the property of being disjoint is right commutative with respect to the infimum operation (`⊓`). In other words, `a` and `b` are disjoint with respect to `c` if and only if `a` and `c` are disjoint with respect to `b`. Here, two elements are said to be disjoint if their greatest lower bound (infimum) is the minimum element of the set.
More concisely: For any semilattice with a minimum element, elements `a`, `b`, and `c` are disjoint with respect to each other if and only if `a ⊓ b = OrderBot` if and only if `a ⊓ c = OrderBot`.
|
eq_top_of_isCompl_bot
theorem eq_top_of_isCompl_bot :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x : α}, IsCompl x ⊥ → x = ⊤
This theorem states that for any type `α` equipped with a lattice structure and a bounded order, if an element `x` of this type is complementary to the bottom element (`⊥`), then `x` is the top element (`⊤`). Essentially, it asserts that in such a structure, the only complement of the bottom element is the top element.
More concisely: In a bounded lattice, the complement of the bottom element is the top element.
|
IsCompl.codisjoint
theorem IsCompl.codisjoint :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → Codisjoint x y := by
sorry
The theorem `IsCompl.codisjoint` states that for any two elements `x` and `y` in a bounded ordered set, if `x` and `y` are complements of each other (denoted by `IsCompl x y`), then `x` and `y` are codisjoint. Codisjointness, in this context, means that for any element in the set that is greater than or equal to both `x` and `y`, the greatest element in the set (denoted by `⊤`) is also less than or equal to this element.
More concisely: For any bounded ordered set and elements x, y with x complementing y (IsCompl x y), if x ≤ z and y ≤ z for some z, then ⊤ ≤ z.
|
Disjoint.mono_right
theorem Disjoint.mono_right :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, b ≤ c → Disjoint a c → Disjoint a b
The theorem `Disjoint.mono_right` states that for any type `α` that has a partial order and a least element (bottom element, `⊥`), and for any three elements `a`, `b`, and `c` of this type, if `b` is less than or equal to `c` and `a` and `c` are disjoint, then `a` and `b` are also disjoint. Here, two elements are said to be disjoint if for every element `x` that is less than or equal to both of them, `x` is also less than or equal to the bottom element. In other words, the disjointness of `a` and `c` is preserved when replacing `c` with an element `b` that is less than or equal to `c`.
More concisely: If `α` is a type with a partial order and a least element, and `a`, `b`, and `c` are elements of `α` such that `b ≤ c` and `a` and `c` are disjoint, then `a` and `b` are also disjoint.
|
Codisjoint.symm
theorem Codisjoint.symm :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] ⦃a b : α⦄, Codisjoint a b → Codisjoint b a := by
sorry
The theorem `Codisjoint.symm` states that for any given type `α` that has a partial order and a top order, if two elements `a` and `b` of this type are codisjoint (i.e., their supremum is the top element), then the property of being codisjoint is symmetrical, meaning that if `a` and `b` are codisjoint, then `b` and `a` are also codisjoint. In mathematical terms, if for all `x` in `α`, `a ≤ x` and `b ≤ x` implies `⊤ ≤ x`, then `b ≤ x` and `a ≤ x` also implies `⊤ ≤ x`.
More concisely: If elements `a` and `b` of a type `α` with partial order and top element are codisjoint, then `b` and `a` are also codisjoint. (i.e., `a` and `b` have the same supremum, which is the top element, thus they are interchangeable in the definition of codisjointness)
|
Disjoint.mono_left
theorem Disjoint.mono_left :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, a ≤ b → Disjoint b c → Disjoint a c
The theorem `Disjoint.mono_left` states that for any partially ordered set with a bottom element, and for any three elements `a`, `b`, and `c` in that set, if `a` is less than or equal to `b`, and `b` and `c` are disjoint (i.e., the infimum of `b` and `c` is the bottom element of the set), then `a` and `c` must also be disjoint. In other words, disjointness is preserved when decreasing the first element of the pair.
More concisely: If `a` is less than or equal to `b`, and `b` and `c` are disjoint elements in a partially ordered set with a bottom element, then `a` and `c` are also disjoint.
|
Disjoint.le_bot
theorem Disjoint.le_bot :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → a ⊓ b ≤ ⊥
The theorem `Disjoint.le_bot` states that for any type `α` equipped with an inf-semilattice structure and a bottom element `⊥`, if two elements `a` and `b` of `α` are disjoint (in the sense that for any `x` in `α`, if `x` is less than or equal to both `a` and `b`, then `x` must also be less than or equal to `⊥`), then the infimum (greatest lower bound) of `a` and `b` is less than or equal to `⊥`. Essentially, this states that the infimum of any two disjoint elements in this structure cannot exceed the bottom element of the structure.
More concisely: If `α` is an inf-semilattice with bottom element `⊥`, and `a` and `b` are disjoint elements of `α`, then `∧(a, b) ≤ ⊥`.
|
disjoint_left_comm
theorem disjoint_left_comm :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b c : α},
Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)
This theorem states that for any type `α` that is a semilattice with infimum and has a bottom element, and for any three elements `a`, `b`, and `c` of `α`, the statement " `a` is disjoint with the infimum of `b` and `c` " is equivalent to the statement " `b` is disjoint with the infimum of `a` and `c` ". Here, two elements of a lattice are said to be disjoint if their infimum is the bottom element.
More concisely: For any semilattice `α` with bottom element, elements `a`, `b`, and `c` in `α`, `a` is disjoint with the infimum of `b` and `c` if and only if `b` is disjoint with the infimum of `a` and `c`.
|
Disjoint.sup_left
theorem Disjoint.sup_left :
∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α},
Disjoint a c → Disjoint b c → Disjoint (a ⊔ b) c
The theorem `Disjoint.sup_left` states that for all types `α` which are under a distributive lattice and have a least element (`OrderBot α`), and for any three elements `a`, `b` and `c` of `α`, if `a` and `c` are disjoint and `b` and `c` are disjoint, then the supremum of `a` and `b` (`a ⊔ b`) and `c` are also disjoint. In other words, in a distributive lattice, if two elements are both disjoint with a third one, then their supremum is also disjoint with the third one.
More concisely: In a distributive lattice with a least element, if two elements are disjoint from a third element, then their supremum is also disjoint from that element.
|
codisjoint_iff
theorem codisjoint_iff :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b ↔ a ⊔ b = ⊤
The theorem `codisjoint_iff` states that for any type `α` which is a semilattice with a supremum operation and also has a top element, and for any two elements `a` and `b` of type `α`, the two elements `a` and `b` are codisjoint if and only if the supremum of `a` and `b` is the top element of the semilattice. Here, 'codisjoint' refers to a condition where, for any element `x` of type `α`, if `a` and `b` are both less than or equal to `x`, then the top element of the semilattice is less than or equal to `x`.
More concisely: For any semilattice with supremum and top element, elements `a` and `b` are codisjoint if and only if their supremum equals the top element.
|
IsCompl.dual
theorem IsCompl.dual :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α},
IsCompl x y → IsCompl (OrderDual.toDual x) (OrderDual.toDual y)
The theorem `IsCompl.dual` states that for any type `α` which is a partial order and a bounded order, and any two elements `x` and `y` of that type, if `x` and `y` are complements of each other (`IsCompl x y`), then the OrderDual (opposite order) of `x` and `y` are also complements of each other (`IsCompl (OrderDual.toDual x) (OrderDual.toDual y)`). Essentially, this theorem claims that the property of being complements is preserved under the operation of taking the opposite order.
More concisely: If `x` and `y` are complements in a bounded and partially ordered type `α`, then the opposite order complements of `x` and `y` are also complements of each other. In Lean notation: `IsCompl x y -> IsCompl (OrderDual.toDual x) (OrderDual.toDual y)`.
|
disjoint_sup_left
theorem disjoint_sup_left :
∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α},
Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c
The theorem `disjoint_sup_left` states that for any type `α` that forms a distributive lattice with a least element (`OrderBot`), and for any three elements `a`, `b`, and `c` of this type, `(a ⊔ b)` is disjoint with `c` if and only if `a` is disjoint with `c` and `b` is disjoint with `c`. Here, two elements are considered disjoint if their infimum (greatest lower bound) is the least element of the lattice.
More concisely: For any distributive lattice with a least element, elements `a`, `b`, and `c` are disjoint if and only if `a` is disjoint with `c` and `b` is disjoint with `c` if and only if their supremum `(a ⊔ b)` is disjoint with `c`.
|
Codisjoint.top_le
theorem Codisjoint.top_le :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → ⊤ ≤ a ⊔ b
The theorem `Codisjoint.top_le` states that for any type `α` that forms a semilattice with a supremum operation and has a top element, and any two elements `a` and `b` of `α`, if `a` and `b` are codisjoint (meaning the supremum of `a` and `b` is the top element), then the top element is less than or equal to the supremum of `a` and `b`. This essentially guarantees that the supremum of any two codisjoint elements in such a structure is the top element.
More concisely: For any semilattice with a top element `α`, if `a` and `b` are codisjoint elements of `α`, then the top element is less than or equal to their supremum.
|
disjoint_self
theorem disjoint_self : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a a ↔ a = ⊥
The theorem `disjoint_self` states that for any partially ordered set which also has the bottom element, an element `a` is disjoint with itself if and only if `a` is the bottom element. This theorem is applicable in the context of lattices where the infimum (greatest lower bound) might not be unique or requires additional decidability conditions. This definition generalizes the concept of disjoint sets in set theory, seen as elements of the subset lattice.
More concisely: In a partially ordered set with a bottom element, an element is disjoint with itself if and only if it is the bottom element.
|
IsCompl.disjoint
theorem IsCompl.disjoint :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → Disjoint x y
The theorem `IsCompl.disjoint` states that for any type `α` that has a partial order and is a bounded order, if two elements `x` and `y` of this type are complementary (denoted by `IsCompl x y`), then `x` and `y` must be disjoint. In other words, for any element `z` of type `α`, if `z` is less than or equal to both `x` and `y`, then `z` must be less than or equal to the bottom element of the order (denoted by `⊥`). This is generalizing the concept of disjoint sets in the context of lattice theory, where two sets are disjoint if their intersection is empty, which corresponds to the infimum being the bottom element.
More concisely: If `α` is a bounded order type with complementary elements `x` and `y` (denoted by `IsCompl x y`), then `x` and `y` have no common lower bounds, that is, for all `z` in `α`, if `z ≤ x` and `z ≤ y`, then `z = ⊥`.
|
IsCompl.of_eq
theorem IsCompl.of_eq :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x y : α}, x ⊓ y = ⊥ → x ⊔ y = ⊤ → IsCompl x y := by
sorry
This theorem, `IsCompl.of_eq`, states that for any types `α` (where `α` is a lattice and a bounded order), and any elements `x` and `y` of `α`, if the infimum (greatest lower bound) of `x` and `y` equals the bottom element (`⊥`), and the supremum (least upper bound) of `x` and `y` equals the top element (`⊤`), then `x` and `y` are said to be complements of each other (denoted as `IsCompl x y`).
More concisely: If `α` is a lattice and bounded order type, `x`, `y` ∈ `α`, `⊥ = inf (x, y)`, and `⊤ = sup (x, y)`, then `x` and `y` are complements of each other (`IsCompl x y`).
|
IsCompl.le_left_iff
theorem IsCompl.le_left_iff :
∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α},
IsCompl x y → (z ≤ x ↔ Disjoint z y)
This theorem states that for any type `α` that has a distributive lattice structure and a bounded order, and for any elements `x`, `y`, and `z` of this type, if `x` and `y` are complements of each other (i.e., their greatest lower bound (infimum) is the bottom element of the lattice and their least upper bound (supremum) is the top element of the lattice), then `z` is less than or equal to `x` if and only if `z` and `y` are disjoint. Here, two elements `a` and `b` are said to be disjoint if for all elements `x` that are less than or equal to `a` and `b`, `x` is also less than or equal to the bottom element of the lattice.
More concisely: For any distributive lattice with a bounded order, elements `x`, `y`, and `z` satisfy `x <= z` if and only if `y` and `z` are disjoint, meaning that for all `a` with `a <= x` and `a <= y`, `a` is the bottom element of the lattice.
|
disjoint_sup_right
theorem disjoint_sup_right :
∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α},
Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c
The theorem `disjoint_sup_right` states that for any type `α`, where `α` is a distributive lattice with a least or bottom element, `Disjoint a (b ⊔ c)` is equivalent to `Disjoint a b` and `Disjoint a c` for any elements `a`, `b`, `c` of `α`. In other words, an element `a` is disjoint with the join (supremum) of elements `b` and `c` if and only if `a` is disjoint with both `b` and `c` separately. Here, two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element of the lattice.
More concisely: In a distributive lattice with least element, an element is disjoint with the join of two other elements if and only if it is disjoint with each of them separately.
|
Codisjoint.mono_right
theorem Codisjoint.mono_right :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b c : α},
b ≤ c → Codisjoint a b → Codisjoint a c
The theorem `Codisjoint.mono_right` states that in a partial order structure with a top element, if we have three elements `a`, `b`, and `c`, and `b` is less than or equal to `c`, then if `a` and `b` are codisjoint, it implies that `a` and `c` are also codisjoint. In other words, the property of being codisjoint is monotonic with respect to the second argument.
More concisely: If `a`, `b`, and `c` are elements of a partial order with a top element, `b` is less than or equal to `c`, and `a` and `b` are codisjoint, then `a` and `c` are also codisjoint.
|
symmetric_disjoint
theorem symmetric_disjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α], Symmetric Disjoint := by
sorry
The `symmetric_disjoint` theorem states that for any type `α` that is a partial order and has a least element (denoted as `⊥`), the disjointness relation is symmetric. In other words, if two elements `a` and `b` of the type `α` are disjoint (meaning any element `x` that is less than or equal to both `a` and `b` is also less than or equal to `⊥`), then `b` and `a` are also disjoint.
More concisely: If `α` is a partial order type with a least element `⊥`, then `a` and `b` are disjoint in `α` if and only if `b` and `a` are disjoint in `α`.
|
Disjoint.eq_bot_of_self
theorem Disjoint.eq_bot_of_self :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a a → a = ⊥
The theorem `Disjoint.eq_bot_of_self` states that for any type `α` with a partial order and a bottom element, if an element `a` of the type `α` is disjoint with itself (meaning the infimum of `a` and `a` is the bottom element), then `a` must be the bottom element of the type `α`. In other words, if the greatest lower bound of a value with itself is the "lowest possible value" in the set, then the value itself must also be this "lowest possible value".
More concisely: If `α` is a type with a partial order and a bottom element, and `a` in `α` is disjoint with itself (i.e., `inf a a` equals the bottom element), then `a` is the bottom element of `α`.
|
Disjoint.symm
theorem Disjoint.symm :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] ⦃a b : α⦄, Disjoint a b → Disjoint b a
This theorem states that the Disjoint property in a lattice is symmetric for any two elements. In other words, for any type `α` that has a partial order and a bottom element, if two elements `a` and `b` are Disjoint (i.e., their greatest lower bound is the bottom element), then `b` and `a` are also Disjoint.
More concisely: For any lattice with bottom element, if elements `a` and `b` are Disjoint, then `b` and `a` are also Disjoint.
|
Codisjoint.mono_left
theorem Codisjoint.mono_left :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b c : α},
a ≤ b → Codisjoint a c → Codisjoint b c
The theorem `Codisjoint.mono_left` states that for any given type `α` that has a partial order and a top element, if we have three elements `a`, `b`, and `c` of this type such that `a` is less than or equal to `b`, and `a` and `c` are codisjoint, then `b` and `c` are also codisjoint. In other words, codisjointness between `a` and `c` implies codisjointness between `b` and `c`. This property can be referred to as the monotonicity of codisjointness on the left side.
More concisely: If `α` is a type with a partial order and a top element, and `a` is less than or equal to `b`, and `a` is codisjoint from `c`, then `b` is codisjoint from `c`.
|
IsCompl.sup_eq_top
theorem IsCompl.sup_eq_top :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → x ⊔ y = ⊤
This theorem states that for any type `α` that forms a lattice and has a bounded order, if `x` and `y` are elements of `α` that are complements of each other (`IsCompl x y`), then the supremum (or join) of `x` and `y`, denoted `x ⊔ y`, is equal to the top element of the lattice, `⊤`. In other words, in a bounded lattice, the supremum of any pair of complementary elements is the greatest element in the lattice.
More concisely: In a bounded lattice, the supremum of any pair of complementary elements is the lattice's top element.
|
disjoint_iff_inf_le
theorem disjoint_iff_inf_le :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b ≤ ⊥
This theorem states that for any type `α` equipped with a semilattice structure and a least element, and for any two elements `a` and `b` from `α`, the two elements `a` and `b` are disjoint if and only if the infimum (greatest lower bound) of `a` and `b` is less than or equal to the least element (denoted as `⊥`). This is a characterization of disjointness in terms of infimum and the bottom element of the lattice. This result connects the concept of disjointness with the order-theoretic operations in the lattice.
More concisely: For any semilattice with least element, elements `a` and `b` are disjoint if and only if their infimum is less than or equal to the least element.
|
Disjoint.inf_right'
theorem Disjoint.inf_right' :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α} (c : α),
Disjoint a b → Disjoint a (c ⊓ b)
The theorem `Disjoint.inf_right'` states that for any type `α` that is a semilattice with respect to the infimum operation (denoted by `⊓`) and has a bottom element (denoted by `⊥`), and for any three elements `a`, `b`, and `c` of `α`, if `a` and `b` are "disjoint" (in the sense that any element less than or equal to both `a` and `b` is also less than or equal to `⊥`), then `a` and `c ⊓ b` are also disjoint. The property of being disjoint is therefore preserved under taking the infimum with `c` on the right.
More concisely: For any semilattice `α` with a bottom element `⊥` and disjoint elements `a` and `b`, `a` and `b ⊓ c` are disjoint for all `c` in `α`.
|
disjoint_assoc
theorem disjoint_assoc :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b c : α},
Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)
The theorem of "disjoint association" states that for any type `α` that is a semilattice with infimum operation and possesses a least element, and any three elements `a`, `b`, and `c` of this type, the property that `a` and `b` infimum is disjoint with `c` is equivalent to the property that `a` is disjoint with the infimum of `b` and `c`. In more mathematical terms, if `Disjoint (a ⊓ b) c` then `Disjoint a (b ⊓ c)` and vice versa. Here, two elements are said to be disjoint if the greatest element that is less than or equal to both of them is the bottom element of the lattice.
More concisely: For any semilattice with infimum and least element `α`, the infima of any two disjoint elements are interchangeable: `Disjoint (a ⊓ b) c <-> Disjoint a (b ⊓ c)`, where `<->` denotes logical equivalence.
|
Disjoint.inf_left'
theorem Disjoint.inf_left' :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α} (c : α),
Disjoint a b → Disjoint (c ⊓ a) b
The theorem `Disjoint.inf_left'` states that for any type `α` that has a semilattice structure with an infimum operation, and a partial order with a bottom element, and for any elements `a`, `b`, and `c` of this type, if `a` and `b` are disjoint (meaning their infimum is the bottom element), then `c` infimum `a` and `b` are also disjoint. This generalizes the notion of intersection (denoted by `⊓`) of two disjoint sets remaining disjoint when intersected with a third set.
More concisely: If `α` is a type with a semilattice and partial order structure having a bottom element, and `a` and `b` are disjoint elements of `α`, then their infimum is the bottom element, and `c` is any element of `α`, then `c` and the infimum of `a` and `b` are disjoint.
|
disjoint_comm
theorem disjoint_comm :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ Disjoint b a
The theorem `disjoint_comm` states that for any type `α` that is equipped with a partial order and a bottom element, the 'disjointness' of two elements `a` and `b` is commutative, i.e., `a` and `b` are disjoint if and only if `b` and `a` are disjoint. In other words, if for all elements `x` in `α`, `x` being less than or equal to `a` and `b` implies `x` is less than or equal to the bottom element, it's equivalent to saying that `x` being less than or equal to `b` and `a` implies `x` is less than or equal to the bottom element.
More concisely: For any type `α` with a partial order and a bottom element, `a` and `b` are disjoint if and only if `b` and `a` are disjoint, i.e., if `x <= a` and `x <= b` implies `x = bottom`, then `x <= b` and `x <= a` implies `x = bottom`.
|
Codisjoint.eq_top
theorem Codisjoint.eq_top :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → a ⊔ b = ⊤
This theorem states that for any type `α` with a semilattice structure and a top element, if two elements `a` and `b` of this type are codisjoint (meaning that for any `x` in `α` such that `a` and `b` are both less than or equal to `x`, the top element `⊤` is less than or equal to `x`), then the supremum of `a` and `b` is exactly `⊤` (the top element). In mathematical terms, this can be written as: if `a` and `b` are codisjoint, then `a ⊔ b = ⊤`.
More concisely: If `α` is a type with a semilattice structure and a top element, and `a` and `b` are codisjoint elements of `α`, then their supremum equals the top element, i.e., `a ⊔ b = ⊤`.
|
Codisjoint.eq_top_of_self
theorem Codisjoint.eq_top_of_self :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, Codisjoint a a → a = ⊤
This theorem, referred to as an alias of the forward direction of `codisjoint_self`, states that for any partial order with a greatest element (denoted by `⊤`), if an element is codisjoint with itself, then that element must be the greatest element of the order. In other words, if for any element `a` in the order (where the order is of some type `α`), it holds that for all `x` such that `a` is less than or equal to `x`, `a` is also less than or equal to `x` and `⊤` is less than or equal to `x`, then `a` is equal to `⊤`.
More concisely: If a partial order with a greatest element `⊤` has an element `a` that is codisjoint with itself (i.e., `a ⊓ x = a` for all `x` with `a ≤ x ≤ ⊤`), then `a` is equal to `⊤`.
|
codisjoint_assoc
theorem codisjoint_assoc :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b c : α},
Codisjoint (a ⊔ b) c ↔ Codisjoint a (b ⊔ c)
The theorem `codisjoint_assoc` states that, for all elements `a`, `b`, and `c` of any type `α` that forms a semilattice with a top element, the property of `a` and `b` joined by the supremum (`⊔`) being codisjoint with `c` is equivalent to `a` being codisjoint with `b` and `c` joined by the supremum. In other words, the codisjointness property is associative with respect to the supremum operation in a lattice.
More concisely: In a semilattice with top element, the codisjointness of `a` with `b` and `b` with `c` implies the codisjointness of `a` with `c` joined by the supremum. Conversely, the codisjointness of `a` with `c` and `c` with the supremum of `a` and `b` implies the codisjointness of `a` with `b`.
|
IsCompl.inf_eq_bot
theorem IsCompl.inf_eq_bot :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → x ⊓ y = ⊥
This theorem states that for any type `α` which forms a lattice and has a bounded order, if `x` and `y` are complement of each other (`IsCompl x y`), then the infimum (greatest lower bound or 'meet') of `x` and `y` is the bottom element (`⊥`) of the lattice. In other words, if two elements are complements in a bounded lattice, their intersection equals the smallest element that exists in the lattice.
More concisely: In a bounded lattice where every element has a complement, the complemented pair forms the greatest lower bound (infimum) of their set.
|
IsCompl.le_sup_right_iff_inf_left_le
theorem IsCompl.le_sup_right_iff_inf_left_le :
∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y a b : α},
IsCompl x y → (a ≤ b ⊔ y ↔ a ⊓ x ≤ b)
This theorem states that in the context of a bounded distributive lattice, for any elements `x`, `y`, `a`, `b` of this lattice, if `x` and `y` are complementary, then the inequality `a` is less than or equal to the join of `b` and `y` holds if and only if the inequality `a` meet `x` is less than or equal to `b` holds. In mathematical notation, if `x` and `y` are complementary (i.e., `x ⊔ y = 1` and `x ⊓ y = 0`), then `a ≤ b ⊔ y` is equivalent to `a ⊓ x ≤ b`.
More concisely: In a bounded distributive lattice, for complementary elements x and y, the inequality a ≤ b holds if and only if a ∧ x ≤ b.
|
Disjoint.le_of_codisjoint
theorem Disjoint.le_of_codisjoint :
∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b c : α},
Disjoint a b → Codisjoint b c → a ≤ c
The theorem states that in a distributive lattice with a bounded order, if two elements 'a' and 'b' are disjoint (i.e., their infimum is the bottom element) and 'b' and another element 'c' are codisjoint (i.e., their supremum is the top element), then 'a' is less than or equal to 'c'.
More concisely: In a distributive lattice with a bounded order, if two elements are disjoint and their complements are codisjoint, then the first element is below the third element.
|
Disjoint.eq_bot
theorem Disjoint.eq_bot :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → a ⊓ b = ⊥
The theorem `Disjoint.eq_bot` states that for any type `α` that forms a semilattice with an infimum operation and has a bottom element, if two elements `a` and `b` of `α` are disjoint (meaning that any element `x` that is less than or equal to both `a` and `b` is also less than or equal to the bottom element), then the infimum of `a` and `b` is the bottom element. In mathematical terms, if `a` and `b` are disjoint in a semilattice, then their greatest lower bound (their infimum) is the smallest element of the lattice.
More concisely: In a semilattice with a bottom element, if `a` and `b` are disjoint elements, then their infimum is the bottom element.
|
IsCompl.symm
theorem IsCompl.symm :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → IsCompl y x
This theorem states that in any partially ordered set that also has a smallest and largest element (a bounded order), for any two elements `x` and `y` in the set, if `x` and `y` are complements of each other (denoted by `IsCompl x y`), then `y` and `x` are also complements of each other (`IsCompl y x`). In other words, the "complement" relation is symmetric.
More concisely: In a bounded partially ordered set, if `x` and `y` are complements of each other, then `y` and `x` are also complements of each other. (IsCompl x y → IsCompl y x)
|
Disjoint.left_le_of_le_sup_right
theorem Disjoint.left_le_of_le_sup_right :
∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α}, a ≤ b ⊔ c → Disjoint a c → a ≤ b := by
sorry
This theorem states that for any type `α` that forms a distributive lattice with a least element (represented by `⊥`), given three elements `a`, `b`, and `c` of this type, if `a` is less than or equal to the supremum (join) of `b` and `c`, and `a` and `c` are disjoint (meaning the greatest lower bound (infimum or meet) of `a` and `c` is the least element `⊥`), then `a` is less than or equal to `b`. In other words, if `a` is below `b` joined with `c` and doesn't intersect with `c`, it must be below `b`.
More concisely: If `α` is a distributive lattice with a least element, and `a ≤ b ∨ c`, `a ∧ c = ⊥`, then `a ≤ b`.
|
codisjoint_left_comm
theorem codisjoint_left_comm :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b c : α},
Codisjoint a (b ⊔ c) ↔ Codisjoint b (a ⊔ c)
The theorem 'codisjoint_left_comm' states that for any type 'α', which is an instance of a semilattice with supremum and has a top order, and any elements 'a', 'b', and 'c' of 'α', the condition of 'a' and the supremum of 'b' and 'c' being codisjoint is equivalent to 'b' and the supremum of 'a' and 'c' being codisjoint. In other words, the property of being codisjoint is left commutative with respect to the supremum operation in this ordered semilattice.
More concisely: In an ordered semilattice with top element where supremums exist, the codisjointness of elements a and the supremum of b and c is equivalent to the codisjointness of b and the supremum of a and c.
|
isCompl_iff
theorem isCompl_iff :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a b : α},
IsCompl a b ↔ Disjoint a b ∧ Codisjoint a b
The theorem `isCompl_iff` states that, for any type `α` that has a partial order and is also a bounded order, two elements `a` and `b` of `α` are complements (as expressed by `IsCompl a b`) if and only if `a` and `b` are both disjoint and codisjoint. In the context of a lattice, two elements are disjoint if their greatest lower bound (infimum) is the least element of the order (`⊥`), while they are codisjoint if their least upper bound (supremum) is the greatest element of the order (`⊤`).
More concisely: In a bounded order, two elements are complements if and only if they have no common lower bound and no common upper bound.
|
disjoint_bot_left
theorem disjoint_bot_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint ⊥ a := by
sorry
This theorem states that for any type `α` that has a structure of a partial order and a bottom element, every element `a` of `α` is disjoint with the bottom element of `α`. Here, two elements of a lattice are defined as disjoint if their greatest lower bound (infimum) is the bottom element. This concept generalizes the idea of disjoint sets, viewed as members of the subset lattice.
More concisely: For any partial order type `α` with a bottom element, every element `a` is disjoint from the bottom element, i.e., their infimum is the bottom element.
|
Disjoint.eq_bot_of_le
theorem Disjoint.eq_bot_of_le :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → a ≤ b → a = ⊥
The theorem `Disjoint.eq_bot_of_le` states that for any partial order with a bottom element, if two elements `a` and `b` are disjoint, and `a` is less than or equal to `b`, then `a` must be equal to the bottom element.
This theorem generalizes the concept of disjointness: in a lattice, two elements are considered disjoint if their greatest lower bound (infimum) is the bottom element. In this context, if one of the disjoint elements is also less than or equal to the other, it must be the bottom element itself.
More concisely: In a partial order with a bottom element, if two disjoint elements `a` and `b` satisfy `a ≤ b`, then `a` is equal to the bottom element.
|