# Products of ordered monoids #

instance Prod.instOrderedAddCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
theorem Prod.instOrderedAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} :
∀ (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.instOrderedCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
• Prod.instOrderedCommMonoid =
instance Prod.instOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
• Prod.instOrderedAddCancelCommMonoid = let __src := inferInstance;
theorem Prod.instOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} :
∀ (x x_1 x_2 : α × β), x + x_1 x + x_2x_1.1 x_2.1 x_1.2 x_2.2
instance Prod.instOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
• Prod.instOrderedCancelCommMonoid = let __src := inferInstance;
abbrev Prod.instExistsAddOfLE.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.instExistsAddOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Add α] [Add β] [] [] :
Equations
• =
abbrev Prod.instExistsAddOfLE.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
instance Prod.instExistsMulOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Mul α] [Mul β] [] [] :
Equations
• =
theorem Prod.instCanonicallyOrderedAddCommMonoid.proof_3 {α : Type u_1} {β : Type u_2} :
∀ (x x_1 : α × β), x.1 (x + x_1).1 x.2 (x + x_1).2
theorem Prod.instCanonicallyOrderedAddCommMonoid.proof_2 {α : Type u_1} {β : Type u_2} :
∀ {a b : α × β}, a b∃ (c : α × β), b = a + c
instance Prod.instCanonicallyOrderedAddCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
• Prod.instCanonicallyOrderedAddCommMonoid = let __src := inferInstance; let __src_1 := inferInstance; let __src_2 := ;
instance Prod.instCanonicallyOrderedCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
• Prod.instCanonicallyOrderedCommMonoid = let __src := inferInstance; let __src_1 := inferInstance; let __src_2 := ;
theorem Prod.Lex.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] :
∀ (x x_1 : Lex (α × β)), x x_1∀ (z : Lex (α × β)), z + x z + x_1
instance Prod.Lex.orderedAddCommMonoid {α : Type u_1} {β : Type u_2} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] :
Equations
instance Prod.Lex.orderedCommMonoid {α : Type u_1} {β : Type u_2} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] :
Equations
• Prod.Lex.orderedCommMonoid =
theorem Prod.Lex.orderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} :
∀ (x x_1 x_2 : Lex (α × β)), x + x_1 x + x_2x_1 x_2
Equations
theorem Prod.Lex.orderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} :
∀ (x x_1 : Lex (α × β)), x x_1∀ (a : Lex (α × β)), a + x a + x_1
instance Prod.Lex.orderedCancelCommMonoid {α : Type u_1} {β : Type u_2} :
Equations
• Prod.Lex.orderedCancelCommMonoid =
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_4 {α : Type u_2} {β : Type u_1} (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} (a : Lex (α × β)) (b : Lex (α × β)) :
a b b a
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) (c : Lex (α × β)) :
a + b a + cb c
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_6 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) :
compare a b =
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) :
a b∀ (c : Lex (α × β)), c + a c + b
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_5 {α : Type u_2} {β : Type u_1} (a : Lex (α × β)) (b : Lex (α × β)) :
max a b = if a b then b else a
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.