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 (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [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 (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [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 (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LE.le] [LocallyFiniteOrderBot α] (a : α) (b : α) : Finset.Iic a + Finset.Iic b ⊆ Finset.Iic (a + b)

theorem Finset.Iic_mul_Iic_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap HMul.hMul) LE.le] [LocallyFiniteOrderBot α] (a : α) (b : α) : Finset.Iic a * Finset.Iic b ⊆ Finset.Iic (a * b)

theorem Finset.Ici_add_Ici_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LE.le] [LocallyFiniteOrderTop α] (a : α) (b : α) : Finset.Ici a + Finset.Ici b ⊆ Finset.Ici (a + b)

theorem Finset.Ici_mul_Ici_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap HMul.hMul) LE.le] [LocallyFiniteOrderTop α] (a : α) (b : α) : Finset.Ici a * Finset.Ici b ⊆ Finset.Ici (a * b)

theorem Finset.Icc_add_Ico_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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 (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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 (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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 (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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 (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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 (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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 (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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 (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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 (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrderBot α] (a : α) (b : α) : Finset.Iic a + Finset.Iio b ⊆ Finset.Iio (a + b)

theorem Finset.Iic_mul_Iio_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrderBot α] (a : α) (b : α) : Finset.Iic a * Finset.Iio b ⊆ Finset.Iio (a * b)

theorem Finset.Iio_add_Iic_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrderBot α] (a : α) (b : α) : Finset.Iio a + Finset.Iic b ⊆ Finset.Iio (a + b)

theorem Finset.Iio_mul_Iic_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrderBot α] (a : α) (b : α) : Finset.Iio a * Finset.Iic b ⊆ Finset.Iio (a * b)

theorem Finset.Ioi_add_Ici_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrderTop α] (a : α) (b : α) : Finset.Ioi a + Finset.Ici b ⊆ Finset.Ioi (a + b)

theorem Finset.Ioi_mul_Ici_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrderTop α] (a : α) (b : α) : Finset.Ioi a * Finset.Ici b ⊆ Finset.Ioi (a * b)

theorem Finset.Ici_add_Ioi_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] [LocallyFiniteOrderTop α] (a : α) (b : α) : Finset.Ici a + Finset.Ioi b ⊆ Finset.Ioi (a + b)

theorem Finset.Ici_mul_Ioi_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] [LocallyFiniteOrderTop α] (a : α) (b : α) : Finset.Ici a * Finset.Ioi b ⊆ Finset.Ioi (a * b)