Documentation

Mathlib.Algebra.Group.Pointwise.Finset.Interval

Pointwise operations on intervals #

This should be kept in sync with Mathlib/Algebra/Order/Group/Pointwise/Interval.lean.

Binary pointwise operations #

Note that the subset operations below only cover the cases with the largest possible intervals on the LHS: to conclude that Ioo a b * Ioo c d ⊆ Ioo (a * c) (c * d), you can use monotonicity of * and Finset.Ico_mul_Ioc_subset.

TODO: repeat these lemmas for the generality of mul_le_mul (which assumes nonnegativity), which the unprimed names have been reserved for

source
theorem Finset.Icc_mul_Icc_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [MulLeftMono α] [MulRightMono α] [LocallyFiniteOrder α] (a b c d : α) :
Icc a b * Icc c d ⊆ Icc (a * c) (b * d)
source
theorem Finset.Icc_add_Icc_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [AddLeftMono α] [AddRightMono α] [LocallyFiniteOrder α] (a b c d : α) :
Icc a b + Icc c d ⊆ Icc (a + c) (b + d)
source
theorem Finset.Iic_mul_Iic_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [MulLeftMono α] [MulRightMono α] [LocallyFiniteOrderBot α] (a b : α) :
Iic a * Iic b ⊆ Iic (a * b)
source
theorem Finset.Iic_add_Iic_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [AddLeftMono α] [AddRightMono α] [LocallyFiniteOrderBot α] (a b : α) :
Iic a + Iic b ⊆ Iic (a + b)
source
theorem Finset.Ici_mul_Ici_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [MulLeftMono α] [MulRightMono α] [LocallyFiniteOrderTop α] (a b : α) :
Ici a * Ici b ⊆ Ici (a * b)
source
theorem Finset.Ici_add_Ici_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [AddLeftMono α] [AddRightMono α] [LocallyFiniteOrderTop α] (a b : α) :
Ici a + Ici b ⊆ Ici (a + b)
source
theorem Finset.Icc_mul_Ico_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) :
Icc a b * Ico c d ⊆ Ico (a * c) (b * d)
source
theorem Finset.Icc_add_Ico_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) :
Icc a b + Ico c d ⊆ Ico (a + c) (b + d)
source
theorem Finset.Ico_mul_Icc_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) :
Ico a b * Icc c d ⊆ Ico (a * c) (b * d)
source
theorem Finset.Ico_add_Icc_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) :
Ico a b + Icc c d ⊆ Ico (a + c) (b + d)
source
theorem Finset.Ioc_mul_Ico_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) :
Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)
source
theorem Finset.Ioc_add_Ico_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) :
Ioc a b + Ico c d ⊆ Ioo (a + c) (b + d)
source
theorem Finset.Ico_mul_Ioc_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) :
Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)
source
theorem Finset.Ico_add_Ioc_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrder α] (a b c d : α) :
Ico a b + Ioc c d ⊆ Ioo (a + c) (b + d)
source
theorem Finset.Iic_mul_Iio_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) :
Iic a * Iio b ⊆ Iio (a * b)
source
theorem Finset.Iic_add_Iio_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) :
Iic a + Iio b ⊆ Iio (a + b)
source
theorem Finset.Iio_mul_Iic_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) :
Iio a * Iic b ⊆ Iio (a * b)
source
theorem Finset.Iio_add_Iic_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) :
Iio a + Iic b ⊆ Iio (a + b)
source
theorem Finset.Ioi_mul_Ici_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) :
Ioi a * Ici b ⊆ Ioi (a * b)
source
theorem Finset.Ioi_add_Ici_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) :
Ioi a + Ici b ⊆ Ioi (a + b)
source
theorem Finset.Ici_mul_Ioi_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) :
Ici a * Ioi b ⊆ Ioi (a * b)
source
theorem Finset.Ici_add_Ioi_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) :
Ici a + Ioi b ⊆ Ioi (a + b)