Documentation

Mathlib.Algebra.Order.Monoid.Prod

Products of ordered monoids #

instance Prod.instOrderedCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCommMonoid α] [OrderedCommMonoid β] :

OrderedCommMonoid (α × β)

Equations

Prod.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯

instance Prod.instOrderedAddCommMonoid {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] :

OrderedAddCommMonoid (α × β)

Equations

Prod.instOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

theorem Prod.instOrderedAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] :

∀ (x x_1 : α × β), x ≤ x_1 → ∀ (x_2 : α × β), (x_2 + x).1 ≤ (x_2 + x_1).1 ∧ (x_2 + x).2 ≤ (x_2 + x_1).2

instance Prod.instOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelCommMonoid α] [OrderedCancelCommMonoid β] :

OrderedCancelCommMonoid (α × β)

Equations

Prod.instOrderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

theorem Prod.instOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :

∀ (x x_1 x_2 : α × β), x + x_1 ≤ x + x_2 → x_1.1 ≤ x_2.1 ∧ x_1.2 ≤ x_2.2

instance Prod.instOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :

OrderedCancelAddCommMonoid (α × β)

Equations

Prod.instOrderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

instance Prod.instExistsMulOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Mul α] [Mul β] [ExistsMulOfLE α] [ExistsMulOfLE β] :

ExistsMulOfLE (α × β)

Equations

⋯ = ⋯

instance Prod.instExistsAddOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Add α] [Add β] [ExistsAddOfLE α] [ExistsAddOfLE β] :

ExistsAddOfLE (α × β)

Equations

⋯ = ⋯

instance Prod.instCanonicallyOrderedCommMonoid {α : Type u_1} {β : Type u_2} [CanonicallyOrderedCommMonoid α] [CanonicallyOrderedCommMonoid β] :

CanonicallyOrderedCommMonoid (α × β)

Equations

Prod.instCanonicallyOrderedCommMonoid = CanonicallyOrderedCommMonoid.mk ⋯ ⋯

theorem Prod.instCanonicallyOrderedAddCommMonoid.proof_2 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] {a : α × β} {b : α × β} :

a ≤ b → ∃ (c : α × β), b = a + c

theorem Prod.instCanonicallyOrderedAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] :

ExistsAddOfLE (α × β)

instance Prod.instCanonicallyOrderedAddCommMonoid {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] :

CanonicallyOrderedAddCommMonoid (α × β)

Equations

Prod.instCanonicallyOrderedAddCommMonoid = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

theorem Prod.instCanonicallyOrderedAddCommMonoid.proof_3 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] :

∀ (x x_1 : α × β), x ≤ x + x_1

instance Prod.Lex.orderedCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCommMonoid α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [OrderedCommMonoid β] :

OrderedCommMonoid (Lex (α × β))

Equations

Prod.Lex.orderedCommMonoid = OrderedCommMonoid.mk ⋯

instance Prod.Lex.orderedAddCommMonoid {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [OrderedAddCommMonoid β] :

OrderedAddCommMonoid (Lex (α × β))

Equations

Prod.Lex.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

theorem Prod.Lex.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [OrderedAddCommMonoid α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [OrderedAddCommMonoid β] :

∀ (x x_1 : Lex (α × β)), x ≤ x_1 → ∀ (z : Lex (α × β)), z + x ≤ z + x_1

instance Prod.Lex.orderedCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelCommMonoid α] [OrderedCancelCommMonoid β] :

OrderedCancelCommMonoid (Lex (α × β))

Equations

Prod.Lex.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

instance Prod.Lex.orderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :

OrderedCancelAddCommMonoid (Lex (α × β))

Equations

Prod.Lex.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

theorem Prod.Lex.orderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :

∀ (x x_1 : Lex (α × β)), x ≤ x_1 → ∀ (a : Lex (α × β)), a + x ≤ a + x_1

theorem Prod.Lex.orderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :

∀ (x x_1 x_2 : Lex (α × β)), x + x_1 ≤ x + x_2 → x_1 ≤ x_2

instance Prod.Lex.linearOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} [LinearOrderedCancelCommMonoid α] [LinearOrderedCancelCommMonoid β] :

LinearOrderedCancelCommMonoid (Lex (α × β))

Equations

Prod.Lex.linearOrderedCancelCommMonoid = LinearOrderedCancelCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) (c : Lex (α × β)) :

a + b ≤ a + c → b ≤ c

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_6 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :

compare a b = compareOfLessAndEq a b

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_5 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :

max a b = if a ≤ b then b else a

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_4 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :

min a b = if a ≤ b then a else b

instance Prod.Lex.linearOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] :

LinearOrderedCancelAddCommMonoid (Lex (α × β))

Equations

Prod.Lex.linearOrderedAddCancelCommMonoid = LinearOrderedCancelAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :

a ≤ b → ∀ (c : Lex (α × β)), c + a ≤ c + b

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :

a ≤ b ∨ b ≤ a