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).1 (x_2 + x_1).1 (x_2 + x).2 (x_2 + x_1).2
Equations
Equations
theorem Prod.instOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :
∀ (x x_1 x_2 : α × β), x + x_1 x + x_2x_1.1 x_2.1 x_1.2 x_2.2
Equations
Equations
abbrev Prod.instExistsAddOfLESumInstAddInstLESum.match_1 {α : Type u_2} {β : Type u_1} [Add β] :
∀ {a b : α × β} (motive : (∃ (c : β), b.2 = a.2 + c)Prop) (x : ∃ (c : β), b.2 = a.2 + c), (∀ (d : β) (hd : b.2 = a.2 + d), motive )motive x
Equations
  • =
Instances For
    abbrev Prod.instExistsAddOfLESumInstAddInstLESum.match_2 {α : Type u_1} {β : Type u_2} [Add α] :
    ∀ {a b : α × β} (motive : (∃ (c : α), b.1 = a.1 + c)Prop) (x : ∃ (c : α), b.1 = a.1 + c), (∀ (c : α) (hc : b.1 = a.1 + c), motive )motive x
    Equations
    • =
    Instances For
      instance Prod.instExistsAddOfLESumInstAddInstLESum {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Add α] [Add β] [ExistsAddOfLE α] [ExistsAddOfLE β] :
      Equations
      • =
      instance Prod.instExistsMulOfLEProdInstMulInstLEProd {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Mul α] [Mul β] [ExistsMulOfLE α] [ExistsMulOfLE β] :
      Equations
      • =
      Equations
      theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_3 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] :
      ∀ (x x_1 : α × β), x.1 (x + x_1).1 x.2 (x + x_1).2
      theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_2 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] :
      ∀ {a b : α × β}, a b∃ (c : α × β), b = a + c
      Equations
      • Prod.instCanonicallyOrderedCommMonoidProd = let __src := inferInstance; let __src_1 := inferInstance; let __src_2 := ; CanonicallyOrderedCommMonoid.mk
      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 x_1 : Lex (α × β)), x x_1∀ (z : Lex (α × β)), z + x z + x_1
      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 β] :
      Equations
      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 β] :
      Equations
      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
      Equations
      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_2x_1 x_2
      Equations
      theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) (c : Lex (α × β)) :
      a + b a + cb c
      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_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_1 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :
      a b∀ (c : Lex (α × β)), c + a c + b
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.