Pi instances for ordered groups and monoids #

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

theorem Pi.orderedAddCommMonoid.proof_2 {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → OrderedAddCommMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) :

a ≤ b → b ≤ a → a = b

source

theorem Pi.orderedAddCommMonoid.proof_3 {ι : Type u_1} {Z : ι → Type u_2} [(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

source

theorem Pi.orderedAddCommMonoid.proof_1 {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → OrderedAddCommMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) :

a + b = b + a

source

instance Pi.orderedAddCommMonoid {ι : Type u_7} {Z : ι → Type u_8} [(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.

source

instance Pi.orderedCommMonoid {ι : Type u_7} {Z : ι → Type u_8} [(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.

source

instance Pi.existsAddOfLe {ι : Type u_7} {α : ι → Type u_8} [(i : ι) → LE (α i)] [(i : ι) → Add (α i)] [∀ (i : ι), ExistsAddOfLE (α i)] :

ExistsAddOfLE ((i : ι) → α i)

Equations

(_ : ExistsAddOfLE ((i : ι) → α i)) = (_ : ExistsAddOfLE ((i : ι) → α i))

source

instance Pi.existsMulOfLe {ι : Type u_7} {α : ι → Type u_8} [(i : ι) → LE (α i)] [(i : ι) → Mul (α i)] [∀ (i : ι), ExistsMulOfLE (α i)] :

ExistsMulOfLE ((i : ι) → α i)

Equations

(_ : ExistsMulOfLE ((i : ι) → α i)) = (_ : ExistsMulOfLE ((i : ι) → α i))

source

theorem Pi.instCanonicallyOrderedAddCommMonoidForAll.proof_4 {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (Z i)] :

∀ {a b : (i : ι) → Z i}, a ≤ b → ∃ (c : (i : ι) → Z i), b = a + c

source

theorem Pi.instCanonicallyOrderedAddCommMonoidForAll.proof_2 {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (Z i)] (a : (i : ι) → Z i) (b : (i : ι) → Z i) :

a ≤ b → ∀ (c : (i : ι) → Z i), c + a ≤ c + b

source

theorem Pi.instCanonicallyOrderedAddCommMonoidForAll.proof_3 {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (Z i)] (a : (i : ι) → Z i) :

⊥ ≤ a

source

theorem Pi.instCanonicallyOrderedAddCommMonoidForAll.proof_5 {ι : Type u_2} {Z : ι → Type u_1} [(i : ι) → CanonicallyOrderedAddCommMonoid (Z i)] :

∀ (x x_1 : (i : ι) → Z i) (x_2 : ι), x x_2 ≤ x x_2 + x_1 x_2

source

instance Pi.instCanonicallyOrderedAddCommMonoidForAll {ι : Type u_7} {Z : ι → Type u_8} [(i : ι) → CanonicallyOrderedAddCommMonoid (Z i)] :

CanonicallyOrderedAddCommMonoid ((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.

source

theorem Pi.instCanonicallyOrderedAddCommMonoidForAll.proof_1 {ι : Type u_1} {Z : ι → Type u_2} [(i : ι) → CanonicallyOrderedAddCommMonoid (Z i)] :

ExistsAddOfLE ((i : ι) → Z i)

source

instance Pi.instCanonicallyOrderedCommMonoidForAll {ι : Type u_7} {Z : ι → Type u_8} [(i : ι) → CanonicallyOrderedCommMonoid (Z i)] :

CanonicallyOrderedCommMonoid ((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.

source

theorem Pi.orderedAddCancelCommMonoid.proof_2 {I : Type u_1} {f : I → Type u_2} [(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

source

theorem Pi.orderedAddCancelCommMonoid.proof_3 {I : Type u_1} {f : I → Type u_2} [(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

source

instance Pi.orderedAddCancelCommMonoid {I : Type u_2} {f : I → Type u_6} [(i : I) → OrderedCancelAddCommMonoid (f i)] :

OrderedCancelAddCommMonoid ((i : I) → f i)

Equations

Pi.orderedAddCancelCommMonoid = let src := Pi.addCommMonoid; OrderedCancelAddCommMonoid.mk (_ : ∀ (x x_1 x_2 : (i : I) → f i), x + x_1 ≤ x + x_2 → ∀ (i : I), x_1 i ≤ x_2 i)

source

theorem Pi.orderedAddCancelCommMonoid.proof_1 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedCancelAddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :

a + b = b + a

source

instance Pi.orderedCancelCommMonoid {I : Type u_2} {f : I → Type u_6} [(i : I) → OrderedCancelCommMonoid (f i)] :

OrderedCancelCommMonoid ((i : I) → f i)

Equations

Pi.orderedCancelCommMonoid = let src := Pi.commMonoid; OrderedCancelCommMonoid.mk (_ : ∀ (x x_1 x_2 : (i : I) → f i), x * x_1 ≤ x * x_2 → ∀ (i : I), x_1 i ≤ x_2 i)

source

theorem Pi.orderedAddCommGroup.proof_5 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :

a - b = a + -b

source

theorem Pi.orderedAddCommGroup.proof_3 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (x : (i : I) → f i) :

AddMonoid.nsmul 0 x = 0

source

theorem Pi.orderedAddCommGroup.proof_10 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :

a + b = b + a

source

theorem Pi.orderedAddCommGroup.proof_9 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :

-a + a = 0

source

theorem Pi.orderedAddCommGroup.proof_2 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :

a + 0 = a

source

theorem Pi.orderedAddCommGroup.proof_6 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :

SubNegMonoid.zsmul 0 a = 0

source

theorem Pi.orderedAddCommGroup.proof_11 {I : Type u_1} {f : I → Type u_2} [(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

source

theorem Pi.orderedAddCommGroup.proof_4 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (n : ℕ) (x : (i : I) → f i) :

AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

source

theorem Pi.orderedAddCommGroup.proof_1 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (a : (i : I) → f i) :

0 + a = a

source

theorem Pi.orderedAddCommGroup.proof_7 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (n : ℕ) (a : (i : I) → f i) :

SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a

source

theorem Pi.orderedAddCommGroup.proof_8 {I : Type u_1} {f : I → Type u_2} [(i : I) → OrderedAddCommGroup (f i)] (n : ℕ) (a : (i : I) → f i) :

SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a

source

instance Pi.orderedAddCommGroup {I : Type u_2} {f : I → Type u_6} [(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)

source

instance Pi.orderedCommGroup {I : Type u_2} {f : I → Type u_6} [(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)

source

instance Pi.orderedSemiring {I : Type u_2} {f : I → Type u_6} [(i : I) → OrderedSemiring (f i)] :

OrderedSemiring ((i : I) → f i)

Equations

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

source

instance Pi.orderedCommSemiring {I : Type u_2} {f : I → Type u_6} [(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)

source

instance Pi.orderedRing {I : Type u_2} {f : I → Type u_6} [(i : I) → OrderedRing (f i)] :

OrderedRing ((i : I) → f i)

Equations

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

source

instance Pi.orderedCommRing {I : Type u_2} {f : I → Type u_6} [(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)

source

theorem Function.const_nonneg_of_nonneg {α : Type u_3} (β : Type u_4) [Zero α] [Preorder α] {a : α} (ha : 0 ≤ a) :

0 ≤ Function.const β a

source

theorem Function.one_le_const_of_one_le {α : Type u_3} (β : Type u_4) [One α] [Preorder α] {a : α} (ha : 1 ≤ a) :

1 ≤ Function.const β a

source

theorem Function.const_nonpos_of_nonpos {α : Type u_3} (β : Type u_4) [Zero α] [Preorder α] {a : α} (ha : a ≤ 0) :

Function.const β a ≤ 0

source

theorem Function.const_le_one_of_le_one {α : Type u_3} (β : Type u_4) [One α] [Preorder α] {a : α} (ha : a ≤ 1) :

Function.const β a ≤ 1

source

@[simp]

theorem Function.const_nonneg {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] {a : α} [Nonempty β] :

0 ≤ Function.const β a ↔ 0 ≤ a

source

@[simp]

theorem Function.one_le_const {α : Type u_3} {β : Type u_4} [One α] [Preorder α] {a : α} [Nonempty β] :

1 ≤ Function.const β a ↔ 1 ≤ a

source

@[simp]

theorem Function.const_pos {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] {a : α} [Nonempty β] :

0 < Function.const β a ↔ 0 < a

source

@[simp]

theorem Function.one_lt_const {α : Type u_3} {β : Type u_4} [One α] [Preorder α] {a : α} [Nonempty β] :

1 < Function.const β a ↔ 1 < a

source

@[simp]

theorem Function.const_nonpos {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] {a : α} [Nonempty β] :

Function.const β a ≤ 0 ↔ a ≤ 0

source

@[simp]

theorem Function.const_le_one {α : Type u_3} {β : Type u_4} [One α] [Preorder α] {a : α} [Nonempty β] :

Function.const β a ≤ 1 ↔ a ≤ 1

source

@[simp]

theorem Function.const_neg {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] {a : α} [Nonempty β] :

Function.const β a < 0 ↔ a < 0

source

@[simp]

theorem Function.const_lt_one {α : Type u_3} {β : Type u_4} [One α] [Preorder α] {a : α} [Nonempty β] :

Function.const β a < 1 ↔ a < 1

source

theorem Function.extend_nonneg {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Zero γ] [LE γ] {f : α → β} {g : α → γ} {e : β → γ} (hg : 0 ≤ g) (he : 0 ≤ e) :

0 ≤ Function.extend f g e

source

theorem Function.one_le_extend {α : Type u_3} {β : Type u_4} {γ : Type u_5} [One γ] [LE γ] {f : α → β} {g : α → γ} {e : β → γ} (hg : 1 ≤ g) (he : 1 ≤ e) :

1 ≤ Function.extend f g e

source

theorem Function.extend_nonpos {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Zero γ] [LE γ] {f : α → β} {g : α → γ} {e : β → γ} (hg : g ≤ 0) (he : e ≤ 0) :

Function.extend f g e ≤ 0

source

theorem Function.extend_le_one {α : Type u_3} {β : Type u_4} {γ : Type u_5} [One γ] [LE γ] {f : α → β} {g : α → γ} {e : β → γ} (hg : g ≤ 1) (he : e ≤ 1) :

Function.extend f g e ≤ 1