mathlib3 documentation

algebra.order.pi

Pi instances for ordered groups and monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def pi.ordered_comm_monoid {ι : Type u_1} {Z : ι Type u_2} [Π (i : ι), ordered_comm_monoid (Z i)] :
ordered_comm_monoid (Π (i : ι), Z i)

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

Equations
@[protected, instance]
def pi.ordered_add_comm_monoid {ι : Type u_1} {Z : ι Type u_2} [Π (i : ι), ordered_add_comm_monoid (Z i)] :
ordered_add_comm_monoid (Π (i : ι), Z i)

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

Equations
@[protected, instance]
def pi.has_exists_add_of_le {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_le (α i)] [Π (i : ι), has_add (α i)] [ (i : ι), has_exists_add_of_le (α i)] :
has_exists_add_of_le (Π (i : ι), α i)
@[protected, instance]
def pi.has_exists_mul_of_le {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_le (α i)] [Π (i : ι), has_mul (α i)] [ (i : ι), has_exists_mul_of_le (α i)] :
has_exists_mul_of_le (Π (i : ι), α i)
theorem function.const_nonneg_of_nonneg {α : Type u_2} (β : Type u_3) [has_zero α] [preorder α] {a : α} (ha : 0 a) :
theorem function.one_le_const_of_one_le {α : Type u_2} (β : Type u_3) [has_one α] [preorder α] {a : α} (ha : 1 a) :
theorem function.const_le_one_of_le_one {α : Type u_2} (β : Type u_3) [has_one α] [preorder α] {a : α} (ha : a 1) :
theorem function.const_nonpos_of_nonpos {α : Type u_2} (β : Type u_3) [has_zero α] [preorder α] {a : α} (ha : a 0) :
@[simp]
theorem function.one_le_const {α : Type u_2} {β : Type u_3} [has_one α] [preorder α] {a : α} [nonempty β] :
@[simp]
theorem function.const_nonneg {α : Type u_2} {β : Type u_3} [has_zero α] [preorder α] {a : α} [nonempty β] :
@[simp]
theorem function.const_pos {α : Type u_2} {β : Type u_3} [has_zero α] [preorder α] {a : α} [nonempty β] :
0 < function.const β a 0 < a
@[simp]
theorem function.one_lt_const {α : Type u_2} {β : Type u_3} [has_one α] [preorder α] {a : α} [nonempty β] :
1 < function.const β a 1 < a
@[simp]
theorem function.const_le_one {α : Type u_2} {β : Type u_3} [has_one α] [preorder α] {a : α} [nonempty β] :
@[simp]
theorem function.const_nonpos {α : Type u_2} {β : Type u_3} [has_zero α] [preorder α] {a : α} [nonempty β] :
@[simp]
theorem function.const_lt_one {α : Type u_2} {β : Type u_3} [has_one α] [preorder α] {a : α} [nonempty β] :
function.const β a < 1 a < 1
@[simp]
theorem function.const_neg {α : Type u_2} {β : Type u_3} [has_zero α] [preorder α] {a : α} [nonempty β] :
function.const β a < 0 a < 0

Extension for the positivity tactic: function.const is positive/nonnegative/nonzero if its input is.