Mathlib.Algebra.Order.Pi

Pi.isOrderedMonoid instance

 {ι : Type*} {Z : ι → Type*} [∀ i, CommMonoid (Z i)] [∀ i, PartialOrder (Z i)] [∀ i, IsOrderedMonoid (Z i)] :
  IsOrderedMonoid (∀ i, Z i)

Full source

/-- The product of a family of ordered commutative monoids is an ordered commutative monoid. -/
@[to_additive
      "The product of a family of ordered additive commutative monoids is
an ordered additive commutative monoid."]
instance isOrderedMonoid {ι : Type*} {Z : ι → Type*} [∀ i, CommMonoid (Z i)]
    [∀ i, PartialOrder (Z i)] [∀ i, IsOrderedMonoid (Z i)] :
    IsOrderedMonoid (∀ i, Z i) where
  mul_le_mul_left _ _ w _ := fun i => mul_le_mul_left' (w i) _

Product of Ordered Commutative Monoids is Ordered Commutative Monoid

Informal description

For any family of types $(Z_i)_{i \in \iota}$ where each $Z_i$ is an ordered commutative monoid, the product type $\prod_{i \in \iota} Z_i$ is also an ordered commutative monoid with pointwise operations and order.

Pi.existsMulOfLe instance

 {ι : Type*} {α : ι → Type*} [∀ i, LE (α i)] [∀ i, Mul (α i)] [∀ i, ExistsMulOfLE (α i)] : ExistsMulOfLE (∀ i, α i)

Full source

@[to_additive]
instance existsMulOfLe {ι : Type*} {α : ι → Type*} [∀ i, LE (α i)] [∀ i, Mul (α i)]
    [∀ i, ExistsMulOfLE (α i)] : ExistsMulOfLE (∀ i, α i) :=
  ⟨fun h =>
    ⟨fun i => (exists_mul_of_le <| h i).choose,
      funext fun i => (exists_mul_of_le <| h i).choose_spec⟩⟩

Existence of Multiplicative Difference in Product Types

Informal description

For any family of types $\alpha_i$ indexed by $ι$, where each $\alpha_i$ is equipped with a multiplication operation and a partial order satisfying the property that for any $x \leq y$ there exists a $z$ such that $y = x * z$, the product type $\prod_{i} \alpha_i$ also satisfies this property.

Pi.instCanonicallyOrderedMulForall instance

 {ι : Type*} {Z : ι → Type*} [∀ i, Monoid (Z i)] [∀ i, PartialOrder (Z i)] [∀ i, CanonicallyOrderedMul (Z i)] :
  CanonicallyOrderedMul (∀ i, Z i)

Full source

/-- The product of a family of canonically ordered monoids is a canonically ordered monoid. -/
@[to_additive
      "The product of a family of canonically ordered additive monoids is
a canonically ordered additive monoid."]
instance {ι : Type*} {Z : ι → Type*} [∀ i, Monoid (Z i)] [∀ i, PartialOrder (Z i)]
    [∀ i, CanonicallyOrderedMul (Z i)] :
    CanonicallyOrderedMul (∀ i, Z i) where
  __ := Pi.existsMulOfLe
  le_self_mul _ _ := fun _ => le_self_mul

Product of Canonically Ordered Monoids is Canonically Ordered

Informal description

For any family of types $(Z_i)_{i \in \iota}$ where each $Z_i$ is a canonically ordered monoid, the product type $\prod_{i \in \iota} Z_i$ is also a canonically ordered monoid with pointwise operations and order.

Pi.isOrderedCancelMonoid instance

 [∀ i, CommMonoid <| f i] [∀ i, PartialOrder <| f i] [∀ i, IsOrderedCancelMonoid <| f i] :
  IsOrderedCancelMonoid (∀ i : I, f i)

Full source

@[to_additive]
instance isOrderedCancelMonoid [∀ i, CommMonoid <| f i] [∀ i, PartialOrder <| f i]
    [∀ i, IsOrderedCancelMonoid <| f i] :
    IsOrderedCancelMonoid (∀ i : I, f i) where
  le_of_mul_le_mul_left _ _ _ h i := le_of_mul_le_mul_left' (h i)

Product of Ordered Cancellative Commutative Monoids is Ordered Cancellative Commutative Monoid

Informal description

For any family of types $(f_i)_{i \in I}$ where each $f_i$ is an ordered cancellative commutative monoid, the product type $\prod_{i \in I} f_i$ is also an ordered cancellative commutative monoid with pointwise operations and order.

Pi.isOrderedRing instance

[∀ i, Semiring (f i)] [∀ i, PartialOrder (f i)] [∀ i, IsOrderedRing (f i)] : IsOrderedRing (∀ i, f i)

Full source

instance isOrderedRing [∀ i, Semiring (f i)] [∀ i, PartialOrder (f i)] [∀ i, IsOrderedRing (f i)] :
    IsOrderedRing (∀ i, f i) where
  add_le_add_left _ _ hab _ := fun _ => add_le_add_left (hab _) _
  zero_le_one := fun i => zero_le_one (α := f i)
  mul_le_mul_of_nonneg_left _ _ _ hab hc := fun _ => mul_le_mul_of_nonneg_left (hab _) <| hc _
  mul_le_mul_of_nonneg_right _ _ _ hab hc := fun _ => mul_le_mul_of_nonneg_right (hab _) <| hc _

Product of Ordered Rings is an Ordered Ring

Informal description

For any family of types $f_i$ indexed by $i$, where each $f_i$ is a semiring with a partial order and satisfies the properties of an ordered ring, the product type $\forall i, f_i$ (the type of functions from the index set to the $f_i$) is also an ordered ring.

Function.one_le_const_of_one_le theorem

(ha : 1 ≤ a) : 1 ≤ const β a

Full source

@[to_additive const_nonneg_of_nonneg]
theorem one_le_const_of_one_le (ha : 1 ≤ a) : 1 ≤ const β a := fun _ => ha

Constant Function Preserves One-Leq Relation

Informal description

For any element $a$ in a type with a partial order and a multiplicative identity, if $1 \leq a$, then the constant function $\text{const}_\beta a$ (which maps every element of $\beta$ to $a$) satisfies $1 \leq \text{const}_\beta a$ pointwise.

Function.const_le_one_of_le_one theorem

(ha : a ≤ 1) : const β a ≤ 1

Full source

@[to_additive]
theorem const_le_one_of_le_one (ha : a ≤ 1) : const β a ≤ 1 := fun _ => ha

Pointwise Inequality for Constant Function: $\text{const}_\beta(a) \leq 1$ when $a \leq 1$

Informal description

For any type $\beta$ and any element $a$ in an ordered monoid, if $a \leq 1$, then the constant function $\text{const}_\beta(a)$ (which maps every element of $\beta$ to $a$) satisfies $\text{const}_\beta(a) \leq 1$ pointwise.

Function.one_le_const theorem

: 1 ≤ const β a ↔ 1 ≤ a

Full source

@[to_additive (attr := simp) const_nonneg]
theorem one_le_const : 1 ≤ const β a ↔ 1 ≤ a :=
  const_le_const

Constant Function Order Comparison: $1 \leq \text{const}_\beta(a) \leftrightarrow 1 \leq a$

Informal description

For any type $\beta$ and element $a$ in an ordered monoid, the constant function $\text{const}_\beta(a)$ (which maps every element of $\beta$ to $a$) satisfies $1 \leq \text{const}_\beta(a)$ if and only if $1 \leq a$.

Function.one_lt_const theorem

: 1 < const β a ↔ 1 < a

Full source

@[to_additive (attr := simp) const_pos]
theorem one_lt_const : 1 < const β a ↔ 1 < a :=
  const_lt_const

Comparison of Constant Function with One: $1 < \text{const}_\beta(a) \leftrightarrow 1 < a$

Informal description

For any type $\beta$ and element $a$ in an ordered monoid, the constant function $\text{const}_\beta(a)$ is greater than $1$ if and only if $a$ is greater than $1$, i.e., $1 < \text{const}_\beta(a) \leftrightarrow 1 < a$.

Function.const_le_one theorem

: const β a ≤ 1 ↔ a ≤ 1

Full source

@[to_additive (attr := simp)]
theorem const_le_one : constconst β a ≤ 1 ↔ a ≤ 1 :=
  const_le_const

Constant Function Inequality: $\text{const}_\beta(a) \leq 1 \leftrightarrow a \leq 1$

Informal description

For any type $\beta$ and element $a$ in an ordered monoid, the constant function $\text{const}_\beta(a)$ is less than or equal to the constant function $1$ if and only if $a \leq 1$.

Function.const_lt_one theorem

: const β a < 1 ↔ a < 1

Full source

@[to_additive (attr := simp) const_neg']
theorem const_lt_one : constconst β a < 1 ↔ a < 1 :=
  const_lt_const

Strict Inequality for Constant Function: $\text{const}_\beta(a) < 1 \leftrightarrow a < 1$

Informal description

For any type $\beta$ and element $a$ in an ordered monoid, the constant function $\text{const}_\beta(a)$ is strictly less than $1$ if and only if $a$ is strictly less than $1$, i.e., $\text{const}_\beta(a) < 1 \leftrightarrow a < 1$.

Function.one_le_extend theorem

(hg : 1 ≤ g) (he : 1 ≤ e) : 1 ≤ extend f g e

Full source

@[to_additive extend_nonneg] lemma one_le_extend (hg : 1 ≤ g) (he : 1 ≤ e) : 1 ≤ extend f g e :=
  fun _b ↦ by classical exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

Extension Preserves Lower Bound of One

Informal description

Given functions $g : \alpha \to \gamma$ and $e : \beta \to \gamma$ such that $1 \leq g$ and $1 \leq e$, the extended function $\text{extend}\,f\,g\,e$ satisfies $1 \leq \text{extend}\,f\,g\,e$ for any function $f : \alpha \to \beta$.

Function.extend_le_one theorem

(hg : g ≤ 1) (he : e ≤ 1) : extend f g e ≤ 1

Full source

@[to_additive] lemma extend_le_one (hg : g ≤ 1) (he : e ≤ 1) : extend f g e ≤ 1 :=
  fun _b ↦ by classical exact dite_le_one (fun _ ↦ hg _) (fun _ ↦ he _)

Extension of Bounded Functions Preserves Upper Bound at One

Informal description

Given functions $f : \alpha \to \beta$, $g : \alpha \to \gamma$, and $e : \beta \to \gamma$ such that $g \leq 1$ and $e \leq 1$, the extended function $\text{extend}\,f\,g\,e$ satisfies $\text{extend}\,f\,g\,e \leq 1$.

Pi.mulSingle_le_mulSingle theorem

: mulSingle i a ≤ mulSingle i b ↔ a ≤ b

Full source

@[to_additive (attr := simp)]
lemma mulSingle_le_mulSingle : mulSinglemulSingle i a ≤ mulSingle i b ↔ a ≤ b := by
  simp [mulSingle, update_le_update_iff]

Inequality of Multiplicative Single Functions at an Index

Informal description

For any index $i$ and elements $a, b$ in the corresponding component of a product type, the inequality $\text{mulSingle}_i(a) \leq \text{mulSingle}_i(b)$ holds if and only if $a \leq b$.

Pi.one_le_mulSingle theorem

: 1 ≤ mulSingle i a ↔ 1 ≤ a

Full source

@[to_additive (attr := simp) single_nonneg]
lemma one_le_mulSingle : 1 ≤ mulSingle i a ↔ 1 ≤ a := by simp [mulSingle]

Inequality between One and Multiplicative Single Function: $1 \leq \text{mulSingle}_i(a) \leftrightarrow 1 \leq a$

Informal description

For any index $i$ and element $a$ in the corresponding component of a product type, the multiplicative identity $1$ is less than or equal to the multiplicative single function $\text{mulSingle}_i(a)$ if and only if $1 \leq a$.

Pi.mulSingle_le_one theorem

: mulSingle i a ≤ 1 ↔ a ≤ 1

Full source

@[to_additive (attr := simp)]
lemma mulSingle_le_one : mulSinglemulSingle i a ≤ 1 ↔ a ≤ 1 := by simp [mulSingle]

Inequality between Multiplicative Single Function and One

Informal description

For any index $i$ and element $a$ in the corresponding component of a product type, the inequality $\text{mulSingle}_i(a) \leq 1$ holds if and only if $a \leq 1$.