add_sup
theorem add_sup :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b c : α),
c + a ⊔ b = (c + a) ⊔ (c + b)
This theorem, `add_sup`, states that for all types `α` that are both a lattice and an additive group, with a covariant class defined for addition and order, the supremum (or least upper bound) of `c + a` and `b` is equal to the supremum of `c + a` and `c + b`. In simpler terms, adding a constant to all elements of a lattice before taking the supremum doesn't change the result.
More concisely: For all types `α` that are both a lattice and an additive group, the supremum of `(a + c)` and `(b + c)` equals `(sup a b) + c`.
|
inf_mul_sup
theorem inf_mul_sup :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a b : α), (a ⊓ b) * (a ⊔ b) = a * b
This theorem states that in any lattice structure `α` that also forms a commutative group, if we have defined a covariant class on `α` under multiplication and the standard order relation (≤), then for any two elements `a` and `b` of `α`, the product of the infimum (greatest lower bound, denoted by a ⊓ b) and the supremum (least upper bound, denoted by a ⊔ b) of `a` and `b` equals the product of `a` and `b`. In mathematical terms, `(a ⊓ b) * (a ⊔ b) = a * b` for all `a` and `b` in `α`.
More concisely: In a commutative lattice-ordered group, the inf infimum and supremum of two elements are multiplicatively idempotent, that is, (inf a b) * (sup a b) = a * b.
|
inf_add_sup
theorem inf_add_sup :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a ⊓ b + a ⊔ b = a + b
This theorem, `inf_add_sup`, states that for any type `α` that is a lattice and an additive commutative group, where the addition operation is covariant, the sum of the infimum (greatest lower bound) and supremum (least upper bound) of any two elements `a` and `b` of type `α` is equal to the sum of `a` and `b`. Essentially, it says that in such a structured type, adding the lowest and highest possible bounds of two elements gives you the same result as simply adding the two elements together.
More concisely: For any lattice and additive commutative group type `α` with covariant addition, the infimum and supremum of `a` and `b` in `α` satisfy `inf a b + sup a b = a + b`.
|
mul_sup
theorem mul_sup :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a b c : α),
c * (a ⊔ b) = c * a ⊔ c * b
This theorem, `mul_sup`, states that for any type `α` that forms both a lattice and a group, and a multiplication operation on `α` that is monotone (meaning that if `x ≤ x_1` then `c * x ≤ c * x_1` for all `c`, `x`, `x_1` in `α`), the product of `c` and the supremum (join or least upper bound) of `a` and `b` equals the supremum of the product of `c` and `a` and the product of `c` and `b`. In terms of algebraic structures, it says that multiplication distributes over the supremum operation in this particular lattice-group structure.
More concisely: For any lattice- and group-structured type `α` with a monotone multiplication, the product of any constant `c` with the supremum of `a` and `b` equals the supremum of the products `c * a` and `c * b`.
|