Documentation

Mathlib.Algebra.Group.Pointwise.Finset.Interval

Pointwise operations on intervals #

This should be kept in sync with Mathlib/Data/Set/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

theorem Finset.Icc_add_Icc_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap HAdd.hAdd) LE.le] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Icc a b + Finset.Icc c d Finset.Icc (a + c) (b + d)
theorem Finset.Icc_mul_Icc_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap HMul.hMul) LE.le] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Icc a b * Finset.Icc c d Finset.Icc (a * c) (b * d)
theorem Finset.Iic_add_Iic_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap HAdd.hAdd) LE.le] [LocallyFiniteOrderBot α] (a : α) (b : α) :
theorem Finset.Iic_mul_Iic_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap HMul.hMul) LE.le] [LocallyFiniteOrderBot α] (a : α) (b : α) :
theorem Finset.Ici_add_Ici_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap HAdd.hAdd) LE.le] [LocallyFiniteOrderTop α] (a : α) (b : α) :
theorem Finset.Ici_mul_Ici_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap HMul.hMul) LE.le] [LocallyFiniteOrderTop α] (a : α) (b : α) :
theorem Finset.Icc_add_Ico_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Icc a b + Finset.Ico c d Finset.Ico (a + c) (b + d)
theorem Finset.Icc_mul_Ico_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Icc a b * Finset.Ico c d Finset.Ico (a * c) (b * d)
theorem Finset.Ico_add_Icc_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Ico a b + Finset.Icc c d Finset.Ico (a + c) (b + d)
theorem Finset.Ico_mul_Icc_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Ico a b * Finset.Icc c d Finset.Ico (a * c) (b * d)
theorem Finset.Ioc_add_Ico_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Ioc a b + Finset.Ico c d Finset.Ioo (a + c) (b + d)
theorem Finset.Ioc_mul_Ico_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Ioc a b * Finset.Ico c d Finset.Ioo (a * c) (b * d)
theorem Finset.Ico_add_Ioc_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Ico a b + Finset.Ioc c d Finset.Ioo (a + c) (b + d)
theorem Finset.Ico_mul_Ioc_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) (d : α) :
Finset.Ico a b * Finset.Ioc c d Finset.Ioo (a * c) (b * d)
theorem Finset.Iic_add_Iio_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrderBot α] (a : α) (b : α) :
theorem Finset.Iic_mul_Iio_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrderBot α] (a : α) (b : α) :
theorem Finset.Iio_add_Iic_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrderBot α] (a : α) (b : α) :
theorem Finset.Iio_mul_Iic_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrderBot α] (a : α) (b : α) :
theorem Finset.Ioi_add_Ici_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrderTop α] (a : α) (b : α) :
theorem Finset.Ioi_mul_Ici_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrderTop α] (a : α) (b : α) :
theorem Finset.Ici_add_Ioi_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrderTop α] (a : α) (b : α) :
theorem Finset.Ici_mul_Ioi_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrderTop α] (a : α) (b : α) :