(Pre)images of intervals #

In this file we prove a bunch of trivial lemmas like “if we add a to all points of [b, c], then we get [a + b, a + c]”. For the functions x ↦ x ± a, x ↦ a ± x, and x ↦ -x we prove lemmas about preimages and images of all intervals. We also prove a few lemmas about images under x ↦ a * x, x ↦ x * a and x ↦ x⁻¹.

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 Set.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 Set.Icc_add_Icc_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LE.le] (a : α) (b : α) (c : α) (d : α) :
Set.Icc a b + Set.Icc c d Set.Icc (a + c) (b + d)
theorem Set.Icc_mul_Icc_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap HMul.hMul) LE.le] (a : α) (b : α) (c : α) (d : α) :
Set.Icc a b * Set.Icc c d Set.Icc (a * c) (b * d)
theorem Set.Iic_add_Iic_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LE.le] (a : α) (b : α) :
+ Set.Iic (a + b)
theorem Set.Iic_mul_Iic_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap HMul.hMul) LE.le] (a : α) (b : α) :
* Set.Iic (a * b)
theorem Set.Ici_add_Ici_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LE.le] (a : α) (b : α) :
+ Set.Ici (a + b)
theorem Set.Ici_mul_Ici_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap HMul.hMul) LE.le] (a : α) (b : α) :
* Set.Ici (a * b)
theorem Set.Icc_add_Ico_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] (a : α) (b : α) (c : α) (d : α) :
Set.Icc a b + Set.Ico c d Set.Ico (a + c) (b + d)
theorem Set.Icc_mul_Ico_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] (a : α) (b : α) (c : α) (d : α) :
Set.Icc a b * Set.Ico c d Set.Ico (a * c) (b * d)
theorem Set.Ico_add_Icc_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] (a : α) (b : α) (c : α) (d : α) :
Set.Ico a b + Set.Icc c d Set.Ico (a + c) (b + d)
theorem Set.Ico_mul_Icc_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] (a : α) (b : α) (c : α) (d : α) :
Set.Ico a b * Set.Icc c d Set.Ico (a * c) (b * d)
theorem Set.Ioc_add_Ico_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] (a : α) (b : α) (c : α) (d : α) :
Set.Ioc a b + Set.Ico c d Set.Ioo (a + c) (b + d)
theorem Set.Ioc_mul_Ico_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] (a : α) (b : α) (c : α) (d : α) :
Set.Ioc a b * Set.Ico c d Set.Ioo (a * c) (b * d)
theorem Set.Ico_add_Ioc_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] (a : α) (b : α) (c : α) (d : α) :
Set.Ico a b + Set.Ioc c d Set.Ioo (a + c) (b + d)
theorem Set.Ico_mul_Ioc_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] (a : α) (b : α) (c : α) (d : α) :
Set.Ico a b * Set.Ioc c d Set.Ioo (a * c) (b * d)
theorem Set.Iic_add_Iio_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] (a : α) (b : α) :
+ Set.Iio (a + b)
theorem Set.Iic_mul_Iio_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] (a : α) (b : α) :
* Set.Iio (a * b)
theorem Set.Iio_add_Iic_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] (a : α) (b : α) :
+ Set.Iio (a + b)
theorem Set.Iio_mul_Iic_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] (a : α) (b : α) :
* Set.Iio (a * b)
theorem Set.Ioi_add_Ici_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] (a : α) (b : α) :
+ Set.Ioi (a + b)
theorem Set.Ioi_mul_Ici_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] (a : α) (b : α) :
* Set.Ioi (a * b)
theorem Set.Ici_add_Ioi_subset {α : Type u_1} [Add α] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HAdd.hAdd) LT.lt] (a : α) (b : α) :
+ Set.Ioi (a + b)
theorem Set.Ici_mul_Ioi_subset' {α : Type u_1} [Mul α] [] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap HMul.hMul) LT.lt] (a : α) (b : α) :
* Set.Ioi (a * b)

Preimages under x ↦ a + x#

@[simp]
theorem Set.preimage_const_add_Ici {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a + x) ⁻¹' = Set.Ici (b - a)
@[simp]
theorem Set.preimage_const_add_Ioi {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a + x) ⁻¹' = Set.Ioi (b - a)
@[simp]
theorem Set.preimage_const_add_Iic {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a + x) ⁻¹' = Set.Iic (b - a)
@[simp]
theorem Set.preimage_const_add_Iio {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a + x) ⁻¹' = Set.Iio (b - a)
@[simp]
theorem Set.preimage_const_add_Icc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a + x) ⁻¹' Set.Icc b c = Set.Icc (b - a) (c - a)
@[simp]
theorem Set.preimage_const_add_Ico {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a + x) ⁻¹' Set.Ico b c = Set.Ico (b - a) (c - a)
@[simp]
theorem Set.preimage_const_add_Ioc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a + x) ⁻¹' Set.Ioc b c = Set.Ioc (b - a) (c - a)
@[simp]
theorem Set.preimage_const_add_Ioo {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a + x) ⁻¹' Set.Ioo b c = Set.Ioo (b - a) (c - a)

Preimages under x ↦ x + a#

@[simp]
theorem Set.preimage_add_const_Ici {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x + a) ⁻¹' = Set.Ici (b - a)
@[simp]
theorem Set.preimage_add_const_Ioi {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x + a) ⁻¹' = Set.Ioi (b - a)
@[simp]
theorem Set.preimage_add_const_Iic {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x + a) ⁻¹' = Set.Iic (b - a)
@[simp]
theorem Set.preimage_add_const_Iio {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x + a) ⁻¹' = Set.Iio (b - a)
@[simp]
theorem Set.preimage_add_const_Icc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x + a) ⁻¹' Set.Icc b c = Set.Icc (b - a) (c - a)
@[simp]
theorem Set.preimage_add_const_Ico {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x + a) ⁻¹' Set.Ico b c = Set.Ico (b - a) (c - a)
@[simp]
theorem Set.preimage_add_const_Ioc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x + a) ⁻¹' Set.Ioc b c = Set.Ioc (b - a) (c - a)
@[simp]
theorem Set.preimage_add_const_Ioo {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x + a) ⁻¹' Set.Ioo b c = Set.Ioo (b - a) (c - a)

Preimages under x ↦ -x#

@[simp]
theorem Set.preimage_neg_Ici {α : Type u_1} (a : α) :
@[simp]
theorem Set.preimage_neg_Iic {α : Type u_1} (a : α) :
@[simp]
theorem Set.preimage_neg_Ioi {α : Type u_1} (a : α) :
@[simp]
theorem Set.preimage_neg_Iio {α : Type u_1} (a : α) :
@[simp]
theorem Set.preimage_neg_Icc {α : Type u_1} (a : α) (b : α) :
-Set.Icc a b = Set.Icc (-b) (-a)
@[simp]
theorem Set.preimage_neg_Ico {α : Type u_1} (a : α) (b : α) :
-Set.Ico a b = Set.Ioc (-b) (-a)
@[simp]
theorem Set.preimage_neg_Ioc {α : Type u_1} (a : α) (b : α) :
-Set.Ioc a b = Set.Ico (-b) (-a)
@[simp]
theorem Set.preimage_neg_Ioo {α : Type u_1} (a : α) (b : α) :
-Set.Ioo a b = Set.Ioo (-b) (-a)

Preimages under x ↦ x - a#

@[simp]
theorem Set.preimage_sub_const_Ici {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x - a) ⁻¹' = Set.Ici (b + a)
@[simp]
theorem Set.preimage_sub_const_Ioi {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x - a) ⁻¹' = Set.Ioi (b + a)
@[simp]
theorem Set.preimage_sub_const_Iic {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x - a) ⁻¹' = Set.Iic (b + a)
@[simp]
theorem Set.preimage_sub_const_Iio {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x - a) ⁻¹' = Set.Iio (b + a)
@[simp]
theorem Set.preimage_sub_const_Icc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) ⁻¹' Set.Icc b c = Set.Icc (b + a) (c + a)
@[simp]
theorem Set.preimage_sub_const_Ico {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) ⁻¹' Set.Ico b c = Set.Ico (b + a) (c + a)
@[simp]
theorem Set.preimage_sub_const_Ioc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) ⁻¹' Set.Ioc b c = Set.Ioc (b + a) (c + a)
@[simp]
theorem Set.preimage_sub_const_Ioo {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) ⁻¹' Set.Ioo b c = Set.Ioo (b + a) (c + a)

Preimages under x ↦ a - x#

@[simp]
theorem Set.preimage_const_sub_Ici {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a - x) ⁻¹' = Set.Iic (a - b)
@[simp]
theorem Set.preimage_const_sub_Iic {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a - x) ⁻¹' = Set.Ici (a - b)
@[simp]
theorem Set.preimage_const_sub_Ioi {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a - x) ⁻¹' = Set.Iio (a - b)
@[simp]
theorem Set.preimage_const_sub_Iio {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a - x) ⁻¹' = Set.Ioi (a - b)
@[simp]
theorem Set.preimage_const_sub_Icc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) ⁻¹' Set.Icc b c = Set.Icc (a - c) (a - b)
@[simp]
theorem Set.preimage_const_sub_Ico {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) ⁻¹' Set.Ico b c = Set.Ioc (a - c) (a - b)
@[simp]
theorem Set.preimage_const_sub_Ioc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) ⁻¹' Set.Ioc b c = Set.Ico (a - c) (a - b)
@[simp]
theorem Set.preimage_const_sub_Ioo {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) ⁻¹' Set.Ioo b c = Set.Ioo (a - c) (a - b)

Images under x ↦ a + x#

theorem Set.image_const_add_Iic {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a + x) '' = Set.Iic (a + b)
theorem Set.image_const_add_Iio {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a + x) '' = Set.Iio (a + b)

Images under x ↦ x + a#

theorem Set.image_add_const_Iic {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x + a) '' = Set.Iic (b + a)
theorem Set.image_add_const_Iio {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x + a) '' = Set.Iio (b + a)

Images under x ↦ -x#

theorem Set.image_neg_Ici {α : Type u_1} (a : α) :
Neg.neg '' = Set.Iic (-a)
theorem Set.image_neg_Iic {α : Type u_1} (a : α) :
Neg.neg '' = Set.Ici (-a)
theorem Set.image_neg_Ioi {α : Type u_1} (a : α) :
Neg.neg '' = Set.Iio (-a)
theorem Set.image_neg_Iio {α : Type u_1} (a : α) :
Neg.neg '' = Set.Ioi (-a)
theorem Set.image_neg_Icc {α : Type u_1} (a : α) (b : α) :
Neg.neg '' Set.Icc a b = Set.Icc (-b) (-a)
theorem Set.image_neg_Ico {α : Type u_1} (a : α) (b : α) :
Neg.neg '' Set.Ico a b = Set.Ioc (-b) (-a)
theorem Set.image_neg_Ioc {α : Type u_1} (a : α) (b : α) :
Neg.neg '' Set.Ioc a b = Set.Ico (-b) (-a)
theorem Set.image_neg_Ioo {α : Type u_1} (a : α) (b : α) :
Neg.neg '' Set.Ioo a b = Set.Ioo (-b) (-a)

Images under x ↦ a - x#

@[simp]
theorem Set.image_const_sub_Ici {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a - x) '' = Set.Iic (a - b)
@[simp]
theorem Set.image_const_sub_Iic {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a - x) '' = Set.Ici (a - b)
@[simp]
theorem Set.image_const_sub_Ioi {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a - x) '' = Set.Iio (a - b)
@[simp]
theorem Set.image_const_sub_Iio {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => a - x) '' = Set.Ioi (a - b)
@[simp]
theorem Set.image_const_sub_Icc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) '' Set.Icc b c = Set.Icc (a - c) (a - b)
@[simp]
theorem Set.image_const_sub_Ico {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) '' Set.Ico b c = Set.Ioc (a - c) (a - b)
@[simp]
theorem Set.image_const_sub_Ioc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) '' Set.Ioc b c = Set.Ico (a - c) (a - b)
@[simp]
theorem Set.image_const_sub_Ioo {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) '' Set.Ioo b c = Set.Ioo (a - c) (a - b)

Images under x ↦ x - a#

@[simp]
theorem Set.image_sub_const_Ici {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x - a) '' = Set.Ici (b - a)
@[simp]
theorem Set.image_sub_const_Iic {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x - a) '' = Set.Iic (b - a)
@[simp]
theorem Set.image_sub_const_Ioi {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x - a) '' = Set.Ioi (b - a)
@[simp]
theorem Set.image_sub_const_Iio {α : Type u_1} (a : α) (b : α) :
(fun (x : α) => x - a) '' = Set.Iio (b - a)
@[simp]
theorem Set.image_sub_const_Icc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) '' Set.Icc b c = Set.Icc (b - a) (c - a)
@[simp]
theorem Set.image_sub_const_Ico {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) '' Set.Ico b c = Set.Ico (b - a) (c - a)
@[simp]
theorem Set.image_sub_const_Ioc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) '' Set.Ioc b c = Set.Ioc (b - a) (c - a)
@[simp]
theorem Set.image_sub_const_Ioo {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) '' Set.Ioo b c = Set.Ioo (b - a) (c - a)

Bijections #

theorem Set.Iic_add_bij {α : Type u_1} (a : α) (b : α) :
Set.BijOn (fun (x : α) => x + a) () (Set.Iic (b + a))
theorem Set.Iio_add_bij {α : Type u_1} (a : α) (b : α) :
Set.BijOn (fun (x : α) => x + a) () (Set.Iio (b + a))
@[simp]
theorem Set.preimage_const_add_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a + x) ⁻¹' Set.uIcc b c = Set.uIcc (b - a) (c - a)
@[simp]
theorem Set.preimage_add_const_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x + a) ⁻¹' Set.uIcc b c = Set.uIcc (b - a) (c - a)
@[simp]
theorem Set.preimage_neg_uIcc {α : Type u_1} (a : α) (b : α) :
-Set.uIcc a b = Set.uIcc (-a) (-b)
@[simp]
theorem Set.preimage_sub_const_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) ⁻¹' Set.uIcc b c = Set.uIcc (b + a) (c + a)
@[simp]
theorem Set.preimage_const_sub_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) ⁻¹' Set.uIcc b c = Set.uIcc (a - b) (a - c)
theorem Set.image_const_add_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a + x) '' Set.uIcc b c = Set.uIcc (a + b) (a + c)
theorem Set.image_add_const_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x + a) '' Set.uIcc b c = Set.uIcc (b + a) (c + a)
@[simp]
theorem Set.image_const_sub_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a - x) '' Set.uIcc b c = Set.uIcc (a - b) (a - c)
@[simp]
theorem Set.image_sub_const_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x - a) '' Set.uIcc b c = Set.uIcc (b - a) (c - a)
theorem Set.image_neg_uIcc {α : Type u_1} (a : α) (b : α) :
Neg.neg '' Set.uIcc a b = Set.uIcc (-a) (-b)
theorem Set.abs_sub_le_of_uIcc_subset_uIcc {α : Type u_1} {a : α} {b : α} {c : α} {d : α} (h : Set.uIcc c d Set.uIcc a b) :
|d - c| |b - a|

If [c, d] is a subinterval of [a, b], then the distance between c and d is less than or equal to that of a and b

theorem Set.abs_sub_left_of_mem_uIcc {α : Type u_1} {a : α} {b : α} {c : α} (h : c Set.uIcc a b) :
|c - a| |b - a|

If c ∈ [a, b], then the distance between a and c is less than or equal to that of a and b

theorem Set.abs_sub_right_of_mem_uIcc {α : Type u_1} {a : α} {b : α} {c : α} (h : c Set.uIcc a b) :
|b - c| |b - a|

If x ∈ [a, b], then the distance between c and b is less than or equal to that of a and b

Multiplication and inverse in a field #

@[simp]
theorem Set.preimage_mul_const_Iio {α : Type u_1} (a : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) ⁻¹' = Set.Iio (a / c)
@[simp]
theorem Set.preimage_mul_const_Ioi {α : Type u_1} (a : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) ⁻¹' = Set.Ioi (a / c)
@[simp]
theorem Set.preimage_mul_const_Iic {α : Type u_1} (a : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) ⁻¹' = Set.Iic (a / c)
@[simp]
theorem Set.preimage_mul_const_Ici {α : Type u_1} (a : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) ⁻¹' = Set.Ici (a / c)
@[simp]
theorem Set.preimage_mul_const_Ioo {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) ⁻¹' Set.Ioo a b = Set.Ioo (a / c) (b / c)
@[simp]
theorem Set.preimage_mul_const_Ioc {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) ⁻¹' Set.Ioc a b = Set.Ioc (a / c) (b / c)
@[simp]
theorem Set.preimage_mul_const_Ico {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) ⁻¹' Set.Ico a b = Set.Ico (a / c) (b / c)
@[simp]
theorem Set.preimage_mul_const_Icc {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) ⁻¹' Set.Icc a b = Set.Icc (a / c) (b / c)
@[simp]
theorem Set.preimage_mul_const_Iio_of_neg {α : Type u_1} (a : α) {c : α} (h : c < 0) :
(fun (x : α) => x * c) ⁻¹' = Set.Ioi (a / c)
@[simp]
theorem Set.preimage_mul_const_Ioi_of_neg {α : Type u_1} (a : α) {c : α} (h : c < 0) :
(fun (x : α) => x * c) ⁻¹' = Set.Iio (a / c)
@[simp]
theorem Set.preimage_mul_const_Iic_of_neg {α : Type u_1} (a : α) {c : α} (h : c < 0) :
(fun (x : α) => x * c) ⁻¹' = Set.Ici (a / c)
@[simp]
theorem Set.preimage_mul_const_Ici_of_neg {α : Type u_1} (a : α) {c : α} (h : c < 0) :
(fun (x : α) => x * c) ⁻¹' = Set.Iic (a / c)
@[simp]
theorem Set.preimage_mul_const_Ioo_of_neg {α : Type u_1} (a : α) (b : α) {c : α} (h : c < 0) :
(fun (x : α) => x * c) ⁻¹' Set.Ioo a b = Set.Ioo (b / c) (a / c)
@[simp]
theorem Set.preimage_mul_const_Ioc_of_neg {α : Type u_1} (a : α) (b : α) {c : α} (h : c < 0) :
(fun (x : α) => x * c) ⁻¹' Set.Ioc a b = Set.Ico (b / c) (a / c)
@[simp]
theorem Set.preimage_mul_const_Ico_of_neg {α : Type u_1} (a : α) (b : α) {c : α} (h : c < 0) :
(fun (x : α) => x * c) ⁻¹' Set.Ico a b = Set.Ioc (b / c) (a / c)
@[simp]
theorem Set.preimage_mul_const_Icc_of_neg {α : Type u_1} (a : α) (b : α) {c : α} (h : c < 0) :
(fun (x : α) => x * c) ⁻¹' Set.Icc a b = Set.Icc (b / c) (a / c)
@[simp]
theorem Set.preimage_const_mul_Iio {α : Type u_1} (a : α) {c : α} (h : 0 < c) :
(fun (x : α) => c * x) ⁻¹' = Set.Iio (a / c)
@[simp]
theorem Set.preimage_const_mul_Ioi {α : Type u_1} (a : α) {c : α} (h : 0 < c) :
(fun (x : α) => c * x) ⁻¹' = Set.Ioi (a / c)
@[simp]
theorem Set.preimage_const_mul_Iic {α : Type u_1} (a : α) {c : α} (h : 0 < c) :
(fun (x : α) => c * x) ⁻¹' = Set.Iic (a / c)
@[simp]
theorem Set.preimage_const_mul_Ici {α : Type u_1} (a : α) {c : α} (h : 0 < c) :
(fun (x : α) => c * x) ⁻¹' = Set.Ici (a / c)
@[simp]
theorem Set.preimage_const_mul_Ioo {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => c * x) ⁻¹' Set.Ioo a b = Set.Ioo (a / c) (b / c)
@[simp]
theorem Set.preimage_const_mul_Ioc {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => c * x) ⁻¹' Set.Ioc a b = Set.Ioc (a / c) (b / c)
@[simp]
theorem Set.preimage_const_mul_Ico {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => c * x) ⁻¹' Set.Ico a b = Set.Ico (a / c) (b / c)
@[simp]
theorem Set.preimage_const_mul_Icc {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => c * x) ⁻¹' Set.Icc a b = Set.Icc (a / c) (b / c)
@[simp]
theorem Set.preimage_const_mul_Iio_of_neg {α : Type u_1} (a : α) {c : α} (h : c < 0) :
(fun (x : α) => c * x) ⁻¹' = Set.Ioi (a / c)
@[simp]
theorem Set.preimage_const_mul_Ioi_of_neg {α : Type u_1} (a : α) {c : α} (h : c < 0) :
(fun (x : α) => c * x) ⁻¹' = Set.Iio (a / c)
@[simp]
theorem Set.preimage_const_mul_Iic_of_neg {α : Type u_1} (a : α) {c : α} (h : c < 0) :
(fun (x : α) => c * x) ⁻¹' = Set.Ici (a / c)
@[simp]
theorem Set.preimage_const_mul_Ici_of_neg {α : Type u_1} (a : α) {c : α} (h : c < 0) :
(fun (x : α) => c * x) ⁻¹' = Set.Iic (a / c)
@[simp]
theorem Set.preimage_const_mul_Ioo_of_neg {α : Type u_1} (a : α) (b : α) {c : α} (h : c < 0) :
(fun (x : α) => c * x) ⁻¹' Set.Ioo a b = Set.Ioo (b / c) (a / c)
@[simp]
theorem Set.preimage_const_mul_Ioc_of_neg {α : Type u_1} (a : α) (b : α) {c : α} (h : c < 0) :
(fun (x : α) => c * x) ⁻¹' Set.Ioc a b = Set.Ico (b / c) (a / c)
@[simp]
theorem Set.preimage_const_mul_Ico_of_neg {α : Type u_1} (a : α) (b : α) {c : α} (h : c < 0) :
(fun (x : α) => c * x) ⁻¹' Set.Ico a b = Set.Ioc (b / c) (a / c)
@[simp]
theorem Set.preimage_const_mul_Icc_of_neg {α : Type u_1} (a : α) (b : α) {c : α} (h : c < 0) :
(fun (x : α) => c * x) ⁻¹' Set.Icc a b = Set.Icc (b / c) (a / c)
@[simp]
theorem Set.preimage_mul_const_uIcc {α : Type u_1} {a : α} (ha : a 0) (b : α) (c : α) :
(fun (x : α) => x * a) ⁻¹' Set.uIcc b c = Set.uIcc (b / a) (c / a)
@[simp]
theorem Set.preimage_const_mul_uIcc {α : Type u_1} {a : α} (ha : a 0) (b : α) (c : α) :
(fun (x : α) => a * x) ⁻¹' Set.uIcc b c = Set.uIcc (b / a) (c / a)
@[simp]
theorem Set.preimage_div_const_uIcc {α : Type u_1} {a : α} (ha : a 0) (b : α) (c : α) :
(fun (x : α) => x / a) ⁻¹' Set.uIcc b c = Set.uIcc (b * a) (c * a)
@[simp]
theorem Set.image_mul_const_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x * a) '' Set.uIcc b c = Set.uIcc (b * a) (c * a)
@[simp]
theorem Set.image_const_mul_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => a * x) '' Set.uIcc b c = Set.uIcc (a * b) (a * c)
@[simp]
theorem Set.image_div_const_uIcc {α : Type u_1} (a : α) (b : α) (c : α) :
(fun (x : α) => x / a) '' Set.uIcc b c = Set.uIcc (b / a) (c / a)
theorem Set.image_mul_right_Icc' {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) '' Set.Icc a b = Set.Icc (a * c) (b * c)
theorem Set.image_mul_right_Icc {α : Type u_1} {a : α} {b : α} {c : α} (hab : a b) (hc : 0 c) :
(fun (x : α) => x * c) '' Set.Icc a b = Set.Icc (a * c) (b * c)
theorem Set.image_mul_left_Icc' {α : Type u_1} {a : α} (h : 0 < a) (b : α) (c : α) :
(fun (x : α) => a * x) '' Set.Icc b c = Set.Icc (a * b) (a * c)
theorem Set.image_mul_left_Icc {α : Type u_1} {a : α} {b : α} {c : α} (ha : 0 a) (hbc : b c) :
(fun (x : α) => a * x) '' Set.Icc b c = Set.Icc (a * b) (a * c)
theorem Set.image_mul_right_Ioo {α : Type u_1} (a : α) (b : α) {c : α} (h : 0 < c) :
(fun (x : α) => x * c) '' Set.Ioo a b = Set.Ioo (a * c) (b * c)
theorem Set.image_mul_left_Ioo {α : Type u_1} {a : α} (h : 0 < a) (b : α) (c : α) :
(fun (x : α) => a * x) '' Set.Ioo b c = Set.Ioo (a * b) (a * c)
theorem Set.inv_Ioo_0_left {α : Type u_1} {a : α} (ha : 0 < a) :

The (pre)image under inv of Ioo 0 a is Ioi a⁻¹.

theorem Set.inv_Ioi {α : Type u_1} {a : α} (ha : 0 < a) :
()⁻¹ =
theorem Set.image_const_mul_Ioi_zero {k : Type u_2} {x : k} (hx : 0 < x) :
(fun (y : k) => x * y) '' =

Images under x ↦ a * x + b#

@[simp]
theorem Set.image_affine_Icc' {α : Type u_1} {a : α} (h : 0 < a) (b : α) (c : α) (d : α) :
(fun (x : α) => a * x + b) '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)