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_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)

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)

theorem Finset.Iic_mul_Iic_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [MulLeftMono α] [MulRightMono α] [LocallyFiniteOrderBot α] (a b : α) : Iic a * Iic b ⊆ Iic (a * b)

theorem Finset.Iic_add_Iic_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [AddLeftMono α] [AddRightMono α] [LocallyFiniteOrderBot α] (a b : α) : Iic a + Iic b ⊆ Iic (a + b)

theorem Finset.Ici_mul_Ici_subset' {α : Type u_1} [Mul α] [Preorder α] [DecidableEq α] [MulLeftMono α] [MulRightMono α] [LocallyFiniteOrderTop α] (a b : α) : Ici a * Ici b ⊆ Ici (a * b)

theorem Finset.Ici_add_Ici_subset {α : Type u_1} [Add α] [Preorder α] [DecidableEq α] [AddLeftMono α] [AddRightMono α] [LocallyFiniteOrderTop α] (a b : α) : Ici a + Ici b ⊆ Ici (a + b)

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)

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)

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)

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)

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)

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)

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)

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)

theorem Finset.Iic_mul_Iio_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) : Iic a * Iio b ⊆ Iio (a * b)

theorem Finset.Iic_add_Iio_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) : Iic a + Iio b ⊆ Iio (a + b)

theorem Finset.Iio_mul_Iic_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) : Iio a * Iic b ⊆ Iio (a * b)

theorem Finset.Iio_add_Iic_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderBot α] (a b : α) : Iio a + Iic b ⊆ Iio (a + b)

theorem Finset.Ioi_mul_Ici_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) : Ioi a * Ici b ⊆ Ioi (a * b)

theorem Finset.Ioi_add_Ici_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) : Ioi a + Ici b ⊆ Ioi (a + b)

theorem Finset.Ici_mul_Ioi_subset' {α : Type u_1} [Mul α] [PartialOrder α] [DecidableEq α] [MulLeftStrictMono α] [MulRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) : Ici a * Ioi b ⊆ Ioi (a * b)

theorem Finset.Ici_add_Ioi_subset {α : Type u_1} [Add α] [PartialOrder α] [DecidableEq α] [AddLeftStrictMono α] [AddRightStrictMono α] [LocallyFiniteOrderTop α] (a b : α) : Ici a + Ioi b ⊆ Ioi (a + b)