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 : α)
:
Finset.Iic a + Finset.Iic b ⊆ Finset.Iic (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 : α)
:
Finset.Iic a * Finset.Iic b ⊆ Finset.Iic (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 : α)
:
Finset.Ici a + Finset.Ici b ⊆ Finset.Ici (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 : α)
:
Finset.Ici a * Finset.Ici b ⊆ Finset.Ici (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 : α)
:
Finset.Iic a + Finset.Iio b ⊆ Finset.Iio (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 : α)
:
Finset.Iic a * Finset.Iio b ⊆ Finset.Iio (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 : α)
:
Finset.Iio a + Finset.Iic b ⊆ Finset.Iio (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 : α)
:
Finset.Iio a * Finset.Iic b ⊆ Finset.Iio (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 : α)
:
Finset.Ioi a + Finset.Ici b ⊆ Finset.Ioi (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 : α)
:
Finset.Ioi a * Finset.Ici b ⊆ Finset.Ioi (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 : α)
:
Finset.Ici a + Finset.Ioi b ⊆ Finset.Ioi (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 : α)
:
Finset.Ici a * Finset.Ioi b ⊆ Finset.Ioi (a * b)