Pi instances for ordered groups and monoids

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

instance Pi.orderedCommMonoid {ι : Type u_6} {Z : ι → Type u_7} [(i : ι) → OrderedCommMonoid (Z i)] : OrderedCommMonoid ((i : ι) → Z i)

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

Equations

• Pi.orderedCommMonoid = { toCommMonoid := Pi.commMonoid, toPartialOrder := Pi.partialOrder, mul_le_mul_left := ⋯ }

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

• Pi.orderedAddCommMonoid = { toAddCommMonoid := Pi.addCommMonoid, toPartialOrder := Pi.partialOrder, add_le_add_left := ⋯ }

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

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

instance Pi.instCanonicallyOrderedMulForall {ι : Type u_6} {Z : ι → Type u_7} [(i : ι) → Monoid (Z i)] [(i : ι) → PartialOrder (Z i)] [∀ (i : ι), CanonicallyOrderedMul (Z i)] : CanonicallyOrderedMul ((i : ι) → Z i)

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

instance Pi.instCanonicallyOrderedAddForall {ι : Type u_6} {Z : ι → Type u_7} [(i : ι) → AddMonoid (Z i)] [(i : ι) → PartialOrder (Z i)] [∀ (i : ι), CanonicallyOrderedAdd (Z i)] : CanonicallyOrderedAdd ((i : ι) → Z i)

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

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

Equations

• Pi.orderedCancelCommMonoid = { toCommMonoid := Pi.commMonoid, toPartialOrder := Pi.partialOrder, mul_le_mul_left := ⋯, le_of_mul_le_mul_left := ⋯ }

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

Equations

• Pi.orderedAddCancelCommMonoid = { toAddCommMonoid := Pi.addCommMonoid, toPartialOrder := Pi.partialOrder, add_le_add_left := ⋯, le_of_add_le_add_left := ⋯ }

instance Pi.orderedCommGroup {I : Type u_1} {f : I → Type u_5} [(i : I) → OrderedCommGroup (f i)] : OrderedCommGroup ((i : I) → f i)

Equations

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

instance Pi.orderedAddCommGroup {I : Type u_1} {f : I → Type u_5} [(i : I) → OrderedAddCommGroup (f i)] : OrderedAddCommGroup ((i : I) → f i)

Equations

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

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

Equations

• Pi.orderedSemiring = { toSemiring := Pi.semiring, toPartialOrder := Pi.partialOrder, add_le_add_left := ⋯, zero_le_one := ⋯, mul_le_mul_of_nonneg_left := ⋯, mul_le_mul_of_nonneg_right := ⋯ }

instance Pi.orderedCommSemiring {I : Type u_1} {f : I → Type u_5} [(i : I) → OrderedCommSemiring (f i)] : OrderedCommSemiring ((i : I) → f i)

Equations

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

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

Equations

• Pi.orderedRing = { toRing := Pi.ring, toPartialOrder := OrderedSemiring.toPartialOrder, add_le_add_left := ⋯, zero_le_one := ⋯, mul_nonneg := ⋯ }

instance Pi.orderedCommRing {I : Type u_1} {f : I → Type u_5} [(i : I) → OrderedCommRing (f i)] : OrderedCommRing ((i : I) → f i)

Equations

• Pi.orderedCommRing = { toRing := CommRing.toRing, toPartialOrder := OrderedRing.toPartialOrder, add_le_add_left := ⋯, zero_le_one := ⋯, mul_nonneg := ⋯, mul_comm := ⋯ }

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

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

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

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

@[simp]

theorem Function.one_le_const {α : Type u_2} {β : Type u_3} [One α] [Preorder α] {a : α} [Nonempty β] : 1 ≤ const β a ↔ 1 ≤ a

@[simp]

theorem Function.const_nonneg {α : Type u_2} {β : Type u_3} [Zero α] [Preorder α] {a : α} [Nonempty β] : 0 ≤ const β a ↔ 0 ≤ a

@[simp]

theorem Function.one_lt_const {α : Type u_2} {β : Type u_3} [One α] [Preorder α] {a : α} [Nonempty β] : 1 < const β a ↔ 1 < a

@[simp]

theorem Function.const_pos {α : Type u_2} {β : Type u_3} [Zero α] [Preorder α] {a : α} [Nonempty β] : 0 < const β a ↔ 0 < a

@[simp]

theorem Function.const_le_one {α : Type u_2} {β : Type u_3} [One α] [Preorder α] {a : α} [Nonempty β] : const β a ≤ 1 ↔ a ≤ 1

@[simp]

theorem Function.const_nonpos {α : Type u_2} {β : Type u_3} [Zero α] [Preorder α] {a : α} [Nonempty β] : const β a ≤ 0 ↔ a ≤ 0

@[simp]

theorem Function.const_lt_one {α : Type u_2} {β : Type u_3} [One α] [Preorder α] {a : α} [Nonempty β] : const β a < 1 ↔ a < 1

@[simp]

theorem Function.const_neg' {α : Type u_2} {β : Type u_3} [Zero α] [Preorder α] {a : α} [Nonempty β] : const β a < 0 ↔ a < 0

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

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

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

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

@[simp]

theorem Pi.mulSingle_le_mulSingle {ι : Type u_6} {α : ι → Type u_7} [DecidableEq ι] [(i : ι) → One (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a b : α i} : mulSingle i a ≤ mulSingle i b ↔ a ≤ b

@[simp]

theorem Pi.single_le_single {ι : Type u_6} {α : ι → Type u_7} [DecidableEq ι] [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a b : α i} : single i a ≤ single i b ↔ a ≤ b

theorem Pi.GCongr.mulSingle_mono {ι : Type u_6} {α : ι → Type u_7} [DecidableEq ι] [(i : ι) → One (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a b : α i} : a ≤ b → mulSingle i a ≤ mulSingle i b

Alias of the reverse direction of Pi.mulSingle_le_mulSingle.

theorem Pi.GCongr.single_mono {ι : Type u_6} {α : ι → Type u_7} [DecidableEq ι] [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a b : α i} : a ≤ b → single i a ≤ single i b

@[simp]

theorem Pi.one_le_mulSingle {ι : Type u_6} {α : ι → Type u_7} [DecidableEq ι] [(i : ι) → One (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a : α i} : 1 ≤ mulSingle i a ↔ 1 ≤ a

@[simp]

theorem Pi.single_nonneg {ι : Type u_6} {α : ι → Type u_7} [DecidableEq ι] [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a : α i} : 0 ≤ single i a ↔ 0 ≤ a

@[simp]

theorem Pi.mulSingle_le_one {ι : Type u_6} {α : ι → Type u_7} [DecidableEq ι] [(i : ι) → One (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a : α i} : mulSingle i a ≤ 1 ↔ a ≤ 1

@[simp]

theorem Pi.single_nonpos {ι : Type u_6} {α : ι → Type u_7} [DecidableEq ι] [(i : ι) → Zero (α i)] [(i : ι) → Preorder (α i)] {i : ι} {a : α i} : single i a ≤ 0 ↔ a ≤ 0