Documentation

Mathlib.Algebra.Order.Pi

Pi instances for ordered groups and monoids #

This file defines instances for ordered group, monoid, and related structures on Pi types.

def Pi.orderedAddCommMonoid.proof_2 {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → OrderedAddCommMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) :
a bb aa = b
Equations
  • (_ : ∀ (a b : (i : ι) → Z i), a bb aa = b) = (_ : ∀ (a b : (i : ι) → Z i), a bb aa = b)
def Pi.orderedAddCommMonoid.proof_3 {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → OrderedAddCommMonoid (Z i)] :
∀ (x x_1 : (i : ι) → Z i), x x_1∀ (x_2 : (i : ι) → Z i) (i : ι), x_2 i + x i x_2 i + x_1 i
Equations
  • (_ : x i + x i x i + x i) = (_ : x i + x i x i + x i)
instance Pi.orderedAddCommMonoid {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → OrderedAddCommMonoid (Z i)] :
OrderedAddCommMonoid ((i : ι) → Z i)

The product of a family of ordered additive commutative monoids is an ordered additive commutative monoid.

Equations
  • One or more equations did not get rendered due to their size.
def Pi.orderedAddCommMonoid.proof_1 {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → OrderedAddCommMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) :
a + b = b + a
Equations
  • (_ : ∀ (a b : (i : ι) → Z i), a + b = b + a) = (_ : ∀ (a b : (i : ι) → Z i), a + b = b + a)
instance Pi.orderedCommMonoid {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → OrderedCommMonoid (Z i)] :
OrderedCommMonoid ((i : ι) → Z i)

The product of a family of ordered commutative monoids is an ordered commutative monoid.

Equations
  • One or more equations did not get rendered due to their size.
instance Pi.existsAddOfLe {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LE (α i)] [inst : (i : ι) → Add (α i)] [inst : ∀ (i : ι), ExistsAddOfLE (α i)] :
ExistsAddOfLE ((i : ι) → α i)
Equations
def Pi.existsAddOfLe.proof_1 {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LE (α i)] [inst : (i : ι) → Add (α i)] [inst : ∀ (i : ι), ExistsAddOfLE (α i)] :
ExistsAddOfLE ((i : ι) → α i)
Equations
instance Pi.existsMulOfLe {ι : Type u_1} {α : ιType u_2} [inst : (i : ι) → LE (α i)] [inst : (i : ι) → Mul (α i)] [inst : ∀ (i : ι), ExistsMulOfLE (α i)] :
ExistsMulOfLE ((i : ι) → α i)
Equations
def Pi.instCanonicallyOrderedAddMonoidForAll.proof_5 {ι : Type u_2} {Z : ιType u_1} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] :
∀ (x x_1 : (i : ι) → Z i) (x_2 : ι), x x_2 x x_2 + x_1 x_2
Equations
  • (_ : x x x x + x x) = (_ : x x x x + x x)
def Pi.instCanonicallyOrderedAddMonoidForAll.proof_4 {ι : Type u_2} {Z : ιType u_1} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] :
∀ {a b : (i : ι) → Z i}, a bc, b = a + c
Equations
  • (_ : a bc, b = a + c) = (_ : a bc, b = a + c)
def Pi.instCanonicallyOrderedAddMonoidForAll.proof_3 {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] (a : (i : ι) → Z i) :
Equations
  • (_ : ∀ (a : (i : ι) → Z i), a) = (_ : ∀ (a : (i : ι) → Z i), a)
def Pi.instCanonicallyOrderedAddMonoidForAll.proof_2 {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) :
a b∀ (c : (i : ι) → Z i), c + a c + b
Equations
  • (_ : ∀ (a b : (i : ι) → Z i), a b∀ (c : (i : ι) → Z i), c + a c + b) = (_ : ∀ (a b : (i : ι) → Z i), a b∀ (c : (i : ι) → Z i), c + a c + b)
instance Pi.instCanonicallyOrderedAddMonoidForAll {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] :
CanonicallyOrderedAddMonoid ((i : ι) → Z i)

The product of a family of canonically ordered additive monoids is a canonically ordered additive monoid.

Equations
  • One or more equations did not get rendered due to their size.
def Pi.instCanonicallyOrderedAddMonoidForAll.proof_1 {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → CanonicallyOrderedAddMonoid (Z i)] :
ExistsAddOfLE ((i : ι) → Z i)
Equations
instance Pi.instCanonicallyOrderedMonoidForAll {ι : Type u_1} {Z : ιType u_2} [inst : (i : ι) → CanonicallyOrderedMonoid (Z i)] :
CanonicallyOrderedMonoid ((i : ι) → Z i)

The product of a family of canonically ordered monoids is a canonically ordered monoid.

Equations
  • One or more equations did not get rendered due to their size.
def Pi.orderedAddCancelCommMonoid.proof_1 {I : Type u_2} {f : IType u_1} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a + b + c = a + (b + c)
Equations
  • (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)) = (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))
def Pi.orderedAddCancelCommMonoid.proof_10 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a bb aa = b
Equations
  • (_ : ∀ (a b : (i : I) → f i), a bb aa = b) = (_ : ∀ (a b : (i : I) → f i), a bb aa = b)
def Pi.orderedAddCancelCommMonoid.proof_11 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] :
∀ (x x_1 : (i : I) → f i), x x_1∀ (h : (i : I) → f i) (i : I), h i + x i h i + x_1 i
Equations
  • (_ : h i + x i h i + x i) = (_ : h i + x i h i + x i)
def Pi.orderedAddCancelCommMonoid.proof_5 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (n : ) (x : (i : I) → f i) :
Equations
def Pi.orderedAddCancelCommMonoid.proof_8 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a bb ca c
Equations
  • (_ : ∀ (a b c : (i : I) → f i), a bb ca c) = (_ : ∀ (a b c : (i : I) → f i), a bb ca c)
def Pi.orderedAddCancelCommMonoid.proof_9 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a < b a b ¬b a
Equations
def Pi.orderedAddCancelCommMonoid.proof_7 {I : Type u_2} {f : IType u_1} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) :
a a
Equations
  • (_ : ∀ (a : (i : I) → f i), a a) = (_ : ∀ (a : (i : I) → f i), a a)
def Pi.orderedAddCancelCommMonoid.proof_3 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
Equations
  • (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)
instance Pi.orderedAddCancelCommMonoid {I : Type u} {f : IType v} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] :
OrderedCancelAddCommMonoid ((i : I) → f i)
Equations
  • One or more equations did not get rendered due to their size.
def Pi.orderedAddCancelCommMonoid.proof_6 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
Equations
  • (_ : ∀ (a b : (i : I) → f i), a + b = b + a) = (_ : ∀ (a b : (i : I) → f i), a + b = b + a)
def Pi.orderedAddCancelCommMonoid.proof_12 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] :
∀ (x x_1 x_2 : (i : I) → f i), x + x_1 x + x_2∀ (i : I), x_1 i x_2 i
Equations
  • (_ : x i x i) = (_ : x i x i)
def Pi.orderedAddCancelCommMonoid.proof_4 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (x : (i : I) → f i) :
Equations
def Pi.orderedAddCancelCommMonoid.proof_2 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
Equations
  • (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)
instance Pi.orderedCancelCommMonoid {I : Type u} {f : IType v} [inst : (i : I) → OrderedCancelCommMonoid (f i)] :
OrderedCancelCommMonoid ((i : I) → f i)
Equations
  • One or more equations did not get rendered due to their size.
def Pi.orderedAddCommGroup.proof_9 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (n : ) (a : (i : I) → f i) :
Equations
  • One or more equations did not get rendered due to their size.
def Pi.orderedAddCommGroup.proof_6 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a - b = a + -b
Equations
  • (_ : ∀ (a b : (i : I) → f i), a - b = a + -b) = (_ : ∀ (a b : (i : I) → f i), a - b = a + -b)
def Pi.orderedAddCommGroup.proof_14 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a < b a b ¬b a
Equations
def Pi.orderedAddCommGroup.proof_12 {I : Type u_2} {f : IType u_1} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :
a a
Equations
  • (_ : ∀ (a : (i : I) → f i), a a) = (_ : ∀ (a : (i : I) → f i), a a)
def Pi.orderedAddCommGroup.proof_3 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :
a + 0 = a
Equations
  • (_ : ∀ (a : (i : I) → f i), a + 0 = a) = (_ : ∀ (a : (i : I) → f i), a + 0 = a)
def Pi.orderedAddCommGroup.proof_2 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :
0 + a = a
Equations
  • (_ : ∀ (a : (i : I) → f i), 0 + a = a) = (_ : ∀ (a : (i : I) → f i), 0 + a = a)
instance Pi.orderedAddCommGroup {I : Type u} {f : IType v} [inst : (i : I) → OrderedAddCommGroup (f i)] :
OrderedAddCommGroup ((i : I) → f i)
Equations
  • Pi.orderedAddCommGroup = let src := Pi.addCommGroup; let src_1 := Pi.orderedAddCommMonoid; OrderedAddCommGroup.mk (_ : ∀ (a b : (i : I) → f i), a b∀ (c : (i : I) → f i), c + a c + b)
def Pi.orderedAddCommGroup.proof_5 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (n : ) (x : (i : I) → f i) :
Equations
def Pi.orderedAddCommGroup.proof_15 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a bb aa = b
Equations
  • (_ : ∀ (a b : (i : I) → f i), a bb aa = b) = (_ : ∀ (a b : (i : I) → f i), a bb aa = b)
def Pi.orderedAddCommGroup.proof_13 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a bb ca c
Equations
  • (_ : ∀ (a b c : (i : I) → f i), a bb ca c) = (_ : ∀ (a b c : (i : I) → f i), a bb ca c)
def Pi.orderedAddCommGroup.proof_11 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
Equations
  • (_ : ∀ (a b : (i : I) → f i), a + b = b + a) = (_ : ∀ (a b : (i : I) → f i), a + b = b + a)
def Pi.orderedAddCommGroup.proof_16 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a b∀ (c : (i : I) → f i), c + a c + b
Equations
  • (_ : ∀ (a b : (i : I) → f i), a b∀ (c : (i : I) → f i), c + a c + b) = (_ : ∀ (a b : (i : I) → f i), a b∀ (c : (i : I) → f i), c + a c + b)
def Pi.orderedAddCommGroup.proof_10 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :
-a + a = 0
Equations
  • (_ : ∀ (a : (i : I) → f i), -a + a = 0) = (_ : ∀ (a : (i : I) → f i), -a + a = 0)
def Pi.orderedAddCommGroup.proof_8 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (n : ) (a : (i : I) → f i) :
Equations
  • One or more equations did not get rendered due to their size.
def Pi.orderedAddCommGroup.proof_7 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :
Equations
def Pi.orderedAddCommGroup.proof_4 {I : Type u_1} {f : IType u_2} [inst : (i : I) → OrderedAddCommGroup (f i)] (x : (i : I) → f i) :
Equations
def Pi.orderedAddCommGroup.proof_1 {I : Type u_2} {f : IType u_1} [inst : (i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a + b + c = a + (b + c)
Equations
  • (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)) = (_ : ∀ (a b c : (i : I) → f i), a + b + c = a + (b + c))
instance Pi.orderedCommGroup {I : Type u} {f : IType v} [inst : (i : I) → OrderedCommGroup (f i)] :
OrderedCommGroup ((i : I) → f i)
Equations
  • Pi.orderedCommGroup = let src := Pi.commGroup; let src_1 := Pi.orderedCommMonoid; OrderedCommGroup.mk (_ : ∀ (a b : (i : I) → f i), a b∀ (c : (i : I) → f i), c * a c * b)
instance Pi.orderedSemiring {I : Type u} {f : IType v} [inst : (i : I) → OrderedSemiring (f i)] :
OrderedSemiring ((i : I) → f i)
Equations
  • One or more equations did not get rendered due to their size.
instance Pi.orderedCommSemiring {I : Type u} {f : IType v} [inst : (i : I) → OrderedCommSemiring (f i)] :
OrderedCommSemiring ((i : I) → f i)
Equations
  • Pi.orderedCommSemiring = let src := Pi.commSemiring; let src_1 := Pi.orderedSemiring; OrderedCommSemiring.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)
instance Pi.orderedRing {I : Type u} {f : IType v} [inst : (i : I) → OrderedRing (f i)] :
OrderedRing ((i : I) → f i)
Equations
  • One or more equations did not get rendered due to their size.
instance Pi.orderedCommRing {I : Type u} {f : IType v} [inst : (i : I) → OrderedCommRing (f i)] :
OrderedCommRing ((i : I) → f i)
Equations
  • Pi.orderedCommRing = let src := Pi.commRing; let src_1 := Pi.orderedRing; OrderedCommRing.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)
theorem Function.const_nonneg_of_nonneg {α : Type u_1} (β : Type u_2) [inst : Zero α] [inst : Preorder α] {a : α} (ha : 0 a) :
theorem Function.one_le_const_of_one_le {α : Type u_1} (β : Type u_2) [inst : One α] [inst : Preorder α] {a : α} (ha : 1 a) :
theorem Function.const_nonpos_of_nonpos {α : Type u_1} (β : Type u_2) [inst : Zero α] [inst : Preorder α] {a : α} (ha : a 0) :
theorem Function.const_le_one_of_le_one {α : Type u_1} (β : Type u_2) [inst : One α] [inst : Preorder α] {a : α} (ha : a 1) :
@[simp]
theorem Function.const_nonneg {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Preorder α] {a : α} [inst : Nonempty β] :
@[simp]
theorem Function.one_le_const {α : Type u_1} {β : Type u_2} [inst : One α] [inst : Preorder α] {a : α} [inst : Nonempty β] :
@[simp]
theorem Function.const_pos {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Preorder α] {a : α} [inst : Nonempty β] :
0 < Function.const β a 0 < a
@[simp]
theorem Function.one_lt_const {α : Type u_1} {β : Type u_2} [inst : One α] [inst : Preorder α] {a : α} [inst : Nonempty β] :
1 < Function.const β a 1 < a
@[simp]
theorem Function.const_nonpos {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Preorder α] {a : α} [inst : Nonempty β] :
@[simp]
theorem Function.const_le_one {α : Type u_1} {β : Type u_2} [inst : One α] [inst : Preorder α] {a : α} [inst : Nonempty β] :
@[simp]
theorem Function.const_neg {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Preorder α] {a : α} [inst : Nonempty β] :
Function.const β a < 0 a < 0
@[simp]
theorem Function.const_lt_one {α : Type u_1} {β : Type u_2} [inst : One α] [inst : Preorder α] {a : α} [inst : Nonempty β] :
Function.const β a < 1 a < 1