Documentation

Mathlib.Algebra.Order.Monoid.Prod

Products of ordered monoids #

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

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

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

OrderedAddCommMonoid (α × β)

Equations

Prod.instOrderedAddCommMonoidSum = OrderedAddCommMonoid.mk (_ : ∀ (x x_1 : α × β), x ≤ x_1 → ∀ (x_2 : α × β), (x_2 + x).fst ≤ (x_2 + x_1).fst ∧ (x_2 + x).snd ≤ (x_2 + x_1).snd)

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

OrderedCommMonoid (α × β)

Equations

Prod.instOrderedCommMonoidProd = OrderedCommMonoid.mk (_ : ∀ (x x_1 : α × β), x ≤ x_1 → ∀ (x_2 : α × β), (x_2 * x).fst ≤ (x_2 * x_1).fst ∧ (x_2 * x).snd ≤ (x_2 * x_1).snd)

theorem Prod.instOrderedAddCancelCommMonoid.proof_1 {M : Type u_1} {N : Type u_2} [OrderedCancelAddCommMonoid M] [OrderedCancelAddCommMonoid N] (a : M × N) (b : M × N) :

a ≤ b → ∀ (c : M × N), c + a ≤ c + b

theorem Prod.instOrderedAddCancelCommMonoid.proof_2 {M : Type u_1} {N : Type u_2} [OrderedCancelAddCommMonoid M] [OrderedCancelAddCommMonoid N] :

∀ (x x_1 x_2 : M × N), x + x_1 ≤ x + x_2 → x_1.fst ≤ x_2.fst ∧ x_1.snd ≤ x_2.snd

instance Prod.instOrderedAddCancelCommMonoid {M : Type u_3} {N : Type u_4} [OrderedCancelAddCommMonoid M] [OrderedCancelAddCommMonoid N] :

OrderedCancelAddCommMonoid (M × N)

Equations

One or more equations did not get rendered due to their size.

instance Prod.instOrderedCancelCommMonoid {M : Type u_3} {N : Type u_4} [OrderedCancelCommMonoid M] [OrderedCancelCommMonoid N] :

OrderedCancelCommMonoid (M × N)

Equations

One or more equations did not get rendered due to their size.

abbrev Prod.instExistsAddOfLESumInstAddInstLESum.match_1 {α : Type u_2} {β : Type u_1} [Add β] :

{a b : α × β} → (motive : (∃ c, b.snd = a.snd + c) → Prop) → ∀ (x : ∃ c, b.snd = a.snd + c), (∀ (d : β) (hd : b.snd = a.snd + d), motive (_ : ∃ c, b.snd = a.snd + c)) → motive x

Equations

Prod.instExistsAddOfLESumInstAddInstLESum.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

Instances For

abbrev Prod.instExistsAddOfLESumInstAddInstLESum.match_2 {α : Type u_1} {β : Type u_2} [Add α] :

{a b : α × β} → (motive : (∃ c, b.fst = a.fst + c) → Prop) → ∀ (x : ∃ c, b.fst = a.fst + c), (∀ (c : α) (hc : b.fst = a.fst + c), motive (_ : ∃ c, b.fst = a.fst + c)) → motive x

Equations

Prod.instExistsAddOfLESumInstAddInstLESum.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

Instances For

theorem Prod.instExistsAddOfLESumInstAddInstLESum.proof_1 {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Add α] [Add β] [ExistsAddOfLE α] [ExistsAddOfLE β] :

ExistsAddOfLE (α × β)

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

ExistsAddOfLE (α × β)

Equations

@Prod.instExistsAddOfLESumInstAddInstLESum = @Prod.instExistsAddOfLESumInstAddInstLESum.proof_1

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

ExistsMulOfLE (α × β)

Equations

@Prod.instExistsMulOfLEProdInstMulInstLEProd = @Prod.instExistsMulOfLEProdInstMulInstLEProd.proof_1

theorem Prod.instCanonicallyOrderedAddMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddMonoid α] [CanonicallyOrderedAddMonoid β] (a : α × β) (b : α × β) :

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

theorem Prod.instCanonicallyOrderedAddMonoidSum.proof_3 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddMonoid α] [CanonicallyOrderedAddMonoid β] (a : α × β) :

theorem Prod.instCanonicallyOrderedAddMonoidSum.proof_4 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddMonoid α] [CanonicallyOrderedAddMonoid β] :

∀ {a b : α × β}, a ≤ b → ∃ c, b = a + c

theorem Prod.instCanonicallyOrderedAddMonoidSum.proof_2 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddMonoid α] [CanonicallyOrderedAddMonoid β] :

ExistsAddOfLE (α × β)

instance Prod.instCanonicallyOrderedAddMonoidSum {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddMonoid α] [CanonicallyOrderedAddMonoid β] :

CanonicallyOrderedAddMonoid (α × β)

Equations

One or more equations did not get rendered due to their size.

theorem Prod.instCanonicallyOrderedAddMonoidSum.proof_5 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddMonoid α] [CanonicallyOrderedAddMonoid β] :

∀ (x x_1 : α × β), x.fst ≤ (x + x_1).fst ∧ x.snd ≤ (x + x_1).snd

instance Prod.instCanonicallyOrderedMonoidProd {α : Type u_1} {β : Type u_2} [CanonicallyOrderedMonoid α] [CanonicallyOrderedMonoid β] :

CanonicallyOrderedMonoid (α × β)

Equations

One or more equations did not get rendered due to their size.

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

OrderedAddCommMonoid (Lex (α × β))

Equations

Prod.Lex.orderedAddCommMonoid = OrderedAddCommMonoid.mk (_ : ∀ (x y : Lex (α × β)), x ≤ y → ∀ (z : Lex (α × β)), z + x ≤ z + y)

theorem Prod.Lex.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [OrderedAddCommMonoid α] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [OrderedAddCommMonoid β] (x : Lex (α × β)) (y : Lex (α × β)) (hxy : x ≤ y) (z : Lex (α × β)) :

z + x ≤ z + y

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

OrderedCommMonoid (Lex (α × β))

Equations

Prod.Lex.orderedCommMonoid = OrderedCommMonoid.mk (_ : ∀ (x y : Lex (α × β)), x ≤ y → ∀ (z : Lex (α × β)), z * x ≤ z * y)

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.orderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :

OrderedCancelAddCommMonoid (Lex (α × β))

Equations

One or more equations did not get rendered due to their size.

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

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

OrderedCancelCommMonoid (Lex (α × β))

Equations

One or more equations did not get rendered due to their size.

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

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

a ≤ b ∨ b ≤ a

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_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_1 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :

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

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

LinearOrderedCancelAddCommMonoid (Lex (α × β))

Equations

One or more equations did not get rendered due to their size.

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

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

LinearOrderedCancelCommMonoid (Lex (α × β))

Equations

One or more equations did not get rendered due to their size.