(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_mul_Icc_subset' {α : Type u_1} [Mul α] [Preorder α] [MulLeftMono α] [MulRightMono α] (a b c d : α) : Icc a b * Icc c d ⊆ Icc (a * c) (b * d)

theorem Set.Icc_add_Icc_subset {α : Type u_1} [Add α] [Preorder α] [AddLeftMono α] [AddRightMono α] (a b c d : α) : Icc a b + Icc c d ⊆ Icc (a + c) (b + d)

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

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

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

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

theorem Set.Icc_mul_Ico_subset' {α : Type u_1} [Mul α] [PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b c d : α) : Icc a b * Ico c d ⊆ Ico (a * c) (b * d)

theorem Set.Icc_add_Ico_subset {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α) : Icc a b + Ico c d ⊆ Ico (a + c) (b + d)

theorem Set.Ico_mul_Icc_subset' {α : Type u_1} [Mul α] [PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b c d : α) : Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

theorem Set.Ico_add_Icc_subset {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α) : Ico a b + Icc c d ⊆ Ico (a + c) (b + d)

theorem Set.Ioc_mul_Ico_subset' {α : Type u_1} [Mul α] [PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b c d : α) : Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)

theorem Set.Ioc_add_Ico_subset {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α) : Ioc a b + Ico c d ⊆ Ioo (a + c) (b + d)

theorem Set.Ico_mul_Ioc_subset' {α : Type u_1} [Mul α] [PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b c d : α) : Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)

theorem Set.Ico_add_Ioc_subset {α : Type u_1} [Add α] [PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α) : Ico a b + Ioc c d ⊆ Ioo (a + c) (b + d)

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

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

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

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

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

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

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

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

@[simp]

theorem Set.smul_Icc {α : Type u_1} [LinearOrderedCommMonoid α] [MulLeftReflectLE α] [ExistsMulOfLE α] (a b c : α) : a • Icc b c = Icc (a * b) (a * c)

@[simp]

theorem Set.vadd_Icc {α : Type u_1} [LinearOrderedAddCommMonoid α] [AddLeftReflectLE α] [ExistsAddOfLE α] (a b c : α) : a +ᵥ Icc b c = Icc (a + b) (a + c)

theorem Set.Icc_mul_Icc {α : Type u_1} [LinearOrderedCommMonoid α] [MulLeftReflectLE α] [ExistsMulOfLE α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : Icc a b * Icc c d = Icc (a * c) (b * d)

theorem Set.Icc_add_Icc {α : Type u_1} [LinearOrderedAddCommMonoid α] [AddLeftReflectLE α] [ExistsAddOfLE α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : Icc a b + Icc c d = Icc (a + c) (b + d)

@[simp]

theorem Set.inv_Ici {α : Type u_1} [OrderedCommGroup α] (a : α) : (Ici a)⁻¹ = Iic a⁻¹

@[simp]

theorem Set.neg_Ici {α : Type u_1} [OrderedAddCommGroup α] (a : α) : -Ici a = Iic (-a)

@[simp]

theorem Set.inv_Iic {α : Type u_1} [OrderedCommGroup α] (a : α) : (Iic a)⁻¹ = Ici a⁻¹

@[simp]

theorem Set.neg_Iic {α : Type u_1} [OrderedAddCommGroup α] (a : α) : -Iic a = Ici (-a)

@[simp]

theorem Set.inv_Ioi {α : Type u_1} [OrderedCommGroup α] (a : α) : (Ioi a)⁻¹ = Iio a⁻¹

@[simp]

theorem Set.neg_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a : α) : -Ioi a = Iio (-a)

@[simp]

theorem Set.inv_Iio {α : Type u_1} [OrderedCommGroup α] (a : α) : (Iio a)⁻¹ = Ioi a⁻¹

@[simp]

theorem Set.neg_Iio {α : Type u_1} [OrderedAddCommGroup α] (a : α) : -Iio a = Ioi (-a)

@[simp]

theorem Set.inv_Icc {α : Type u_1} [OrderedCommGroup α] (a b : α) : (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹

@[simp]

theorem Set.neg_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Icc a b = Icc (-b) (-a)

@[simp]

theorem Set.inv_Ico {α : Type u_1} [OrderedCommGroup α] (a b : α) : (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹

@[simp]

theorem Set.neg_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Ico a b = Ioc (-b) (-a)

@[simp]

theorem Set.inv_Ioc {α : Type u_1} [OrderedCommGroup α] (a b : α) : (Ioc a b)⁻¹ = Ico b⁻¹ a⁻¹

@[simp]

theorem Set.neg_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Ioc a b = Ico (-b) (-a)

@[simp]

theorem Set.inv_Ioo {α : Type u_1} [OrderedCommGroup α] (a b : α) : (Ioo a b)⁻¹ = Ioo b⁻¹ a⁻¹

@[simp]

theorem Set.neg_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Ioo a b = Ioo (-b) (-a)

@[deprecated Set.neg_Ici (since := "2024-11-23")]

theorem Set.preimage_neg_Ici {α : Type u_1} [OrderedAddCommGroup α] (a : α) : -Ici a = Iic (-a)

Alias of Set.neg_Ici.

@[deprecated Set.neg_Iic (since := "2024-11-23")]

theorem Set.preimage_neg_Iic {α : Type u_1} [OrderedAddCommGroup α] (a : α) : -Iic a = Ici (-a)

Alias of Set.neg_Iic.

@[deprecated Set.neg_Ioi (since := "2024-11-23")]

theorem Set.preimage_neg_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a : α) : -Ioi a = Iio (-a)

Alias of Set.neg_Ioi.

@[deprecated Set.neg_Iio (since := "2024-11-23")]

theorem Set.preimage_neg_Iio {α : Type u_1} [OrderedAddCommGroup α] (a : α) : -Iio a = Ioi (-a)

Alias of Set.neg_Iio.

@[deprecated Set.neg_Icc (since := "2024-11-23")]

theorem Set.preimage_neg_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Icc a b = Icc (-b) (-a)

Alias of Set.neg_Icc.

@[deprecated Set.neg_Ico (since := "2024-11-23")]

theorem Set.preimage_neg_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Ico a b = Ioc (-b) (-a)

Alias of Set.neg_Ico.

@[deprecated Set.neg_Ioc (since := "2024-11-23")]

theorem Set.preimage_neg_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Ioc a b = Ico (-b) (-a)

Alias of Set.neg_Ioc.

@[deprecated Set.neg_Ioo (since := "2024-11-23")]

theorem Set.preimage_neg_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : -Ioo a b = Ioo (-b) (-a)

Alias of Set.neg_Ioo.

Preimages under x ↦ a + x

@[simp]

theorem Set.preimage_const_add_Ici {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a + x) ⁻¹' Ici b = Ici (b - a)

@[simp]

theorem Set.preimage_const_add_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a + x) ⁻¹' Ioi b = Ioi (b - a)

@[simp]

theorem Set.preimage_const_add_Iic {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a + x) ⁻¹' Iic b = Iic (b - a)

@[simp]

theorem Set.preimage_const_add_Iio {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a + x) ⁻¹' Iio b = Iio (b - a)

@[simp]

theorem Set.preimage_const_add_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a)

@[simp]

theorem Set.preimage_const_add_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a + x) ⁻¹' Ico b c = Ico (b - a) (c - a)

@[simp]

theorem Set.preimage_const_add_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a + x) ⁻¹' Ioc b c = Ioc (b - a) (c - a)

@[simp]

theorem Set.preimage_const_add_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a + x) ⁻¹' Ioo b c = Ioo (b - a) (c - a)

Preimages under x ↦ x + a

@[simp]

theorem Set.preimage_add_const_Ici {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x + a) ⁻¹' Ici b = Ici (b - a)

@[simp]

theorem Set.preimage_add_const_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x + a) ⁻¹' Ioi b = Ioi (b - a)

@[simp]

theorem Set.preimage_add_const_Iic {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x + a) ⁻¹' Iic b = Iic (b - a)

@[simp]

theorem Set.preimage_add_const_Iio {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x + a) ⁻¹' Iio b = Iio (b - a)

@[simp]

theorem Set.preimage_add_const_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x + a) ⁻¹' Icc b c = Icc (b - a) (c - a)

@[simp]

theorem Set.preimage_add_const_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a)

@[simp]

theorem Set.preimage_add_const_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a)

@[simp]

theorem Set.preimage_add_const_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x + a) ⁻¹' Ioo b c = Ioo (b - a) (c - a)

Preimages under x ↦ x - a

@[simp]

theorem Set.preimage_sub_const_Ici {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x - a) ⁻¹' Ici b = Ici (b + a)

@[simp]

theorem Set.preimage_sub_const_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x - a) ⁻¹' Ioi b = Ioi (b + a)

@[simp]

theorem Set.preimage_sub_const_Iic {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x - a) ⁻¹' Iic b = Iic (b + a)

@[simp]

theorem Set.preimage_sub_const_Iio {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x - a) ⁻¹' Iio b = Iio (b + a)

@[simp]

theorem Set.preimage_sub_const_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) ⁻¹' Icc b c = Icc (b + a) (c + a)

@[simp]

theorem Set.preimage_sub_const_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) ⁻¹' Ico b c = Ico (b + a) (c + a)

@[simp]

theorem Set.preimage_sub_const_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) ⁻¹' Ioc b c = Ioc (b + a) (c + a)

@[simp]

theorem Set.preimage_sub_const_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) ⁻¹' Ioo b c = Ioo (b + a) (c + a)

Preimages under x ↦ a - x

@[simp]

theorem Set.preimage_const_sub_Ici {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a - x) ⁻¹' Ici b = Iic (a - b)

@[simp]

theorem Set.preimage_const_sub_Iic {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a - x) ⁻¹' Iic b = Ici (a - b)

@[simp]

theorem Set.preimage_const_sub_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a - x) ⁻¹' Ioi b = Iio (a - b)

@[simp]

theorem Set.preimage_const_sub_Iio {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a - x) ⁻¹' Iio b = Ioi (a - b)

@[simp]

theorem Set.preimage_const_sub_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b)

@[simp]

theorem Set.preimage_const_sub_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) ⁻¹' Ico b c = Ioc (a - c) (a - b)

@[simp]

theorem Set.preimage_const_sub_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b)

@[simp]

theorem Set.preimage_const_sub_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) ⁻¹' Ioo b c = Ioo (a - c) (a - b)

Images under x ↦ a + x

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

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

Images under x ↦ x + a

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

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

Images under x ↦ -x

theorem Set.image_neg_Ici {α : Type u_1} [OrderedAddCommGroup α] (a : α) : Neg.neg '' Ici a = Iic (-a)

theorem Set.image_neg_Iic {α : Type u_1} [OrderedAddCommGroup α] (a : α) : Neg.neg '' Iic a = Ici (-a)

theorem Set.image_neg_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a : α) : Neg.neg '' Ioi a = Iio (-a)

theorem Set.image_neg_Iio {α : Type u_1} [OrderedAddCommGroup α] (a : α) : Neg.neg '' Iio a = Ioi (-a)

theorem Set.image_neg_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : Neg.neg '' Icc a b = Icc (-b) (-a)

theorem Set.image_neg_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : Neg.neg '' Ico a b = Ioc (-b) (-a)

theorem Set.image_neg_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : Neg.neg '' Ioc a b = Ico (-b) (-a)

theorem Set.image_neg_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : Neg.neg '' Ioo a b = Ioo (-b) (-a)

Images under x ↦ a - x

@[simp]

theorem Set.image_const_sub_Ici {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a - x) '' Ici b = Iic (a - b)

@[simp]

theorem Set.image_const_sub_Iic {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a - x) '' Iic b = Ici (a - b)

@[simp]

theorem Set.image_const_sub_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a - x) '' Ioi b = Iio (a - b)

@[simp]

theorem Set.image_const_sub_Iio {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => a - x) '' Iio b = Ioi (a - b)

@[simp]

theorem Set.image_const_sub_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) '' Icc b c = Icc (a - c) (a - b)

@[simp]

theorem Set.image_const_sub_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) '' Ico b c = Ioc (a - c) (a - b)

@[simp]

theorem Set.image_const_sub_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) '' Ioc b c = Ico (a - c) (a - b)

@[simp]

theorem Set.image_const_sub_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) '' Ioo b c = Ioo (a - c) (a - b)

Images under x ↦ x - a

@[simp]

theorem Set.image_sub_const_Ici {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x - a) '' Ici b = Ici (b - a)

@[simp]

theorem Set.image_sub_const_Iic {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x - a) '' Iic b = Iic (b - a)

@[simp]

theorem Set.image_sub_const_Ioi {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x - a) '' Ioi b = Ioi (b - a)

@[simp]

theorem Set.image_sub_const_Iio {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : (fun (x : α) => x - a) '' Iio b = Iio (b - a)

@[simp]

theorem Set.image_sub_const_Icc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) '' Icc b c = Icc (b - a) (c - a)

@[simp]

theorem Set.image_sub_const_Ico {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) '' Ico b c = Ico (b - a) (c - a)

@[simp]

theorem Set.image_sub_const_Ioc {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) '' Ioc b c = Ioc (b - a) (c - a)

@[simp]

theorem Set.image_sub_const_Ioo {α : Type u_1} [OrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) '' Ioo b c = Ioo (b - a) (c - a)

Bijections

theorem Set.Iic_add_bij {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : BijOn (fun (x : α) => x + a) (Iic b) (Iic (b + a))

theorem Set.Iio_add_bij {α : Type u_1} [OrderedAddCommGroup α] (a b : α) : BijOn (fun (x : α) => x + a) (Iio b) (Iio (b + a))

@[simp]

theorem Set.inv_uIcc {α : Type u_1} [LinearOrderedCommGroup α] (a b : α) : (uIcc a b)⁻¹ = uIcc a⁻¹ b⁻¹

@[simp]

theorem Set.neg_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b : α) : -uIcc a b = uIcc (-a) (-b)

@[simp]

theorem Set.preimage_const_add_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a + x) ⁻¹' uIcc b c = uIcc (b - a) (c - a)

@[simp]

theorem Set.preimage_add_const_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x + a) ⁻¹' uIcc b c = uIcc (b - a) (c - a)

@[deprecated Set.neg_uIcc (since := "2024-11-23")]

theorem Set.preimage_neg_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b : α) : -uIcc a b = uIcc (-a) (-b)

@[simp]

theorem Set.preimage_sub_const_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) ⁻¹' uIcc b c = uIcc (b + a) (c + a)

@[simp]

theorem Set.preimage_const_sub_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) ⁻¹' uIcc b c = uIcc (a - b) (a - c)

theorem Set.image_const_add_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a + x) '' uIcc b c = uIcc (a + b) (a + c)

theorem Set.image_add_const_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x + a) '' uIcc b c = uIcc (b + a) (c + a)

@[simp]

theorem Set.image_const_sub_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b c : α) : (fun (x : α) => a - x) '' uIcc b c = uIcc (a - b) (a - c)

@[simp]

theorem Set.image_sub_const_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b c : α) : (fun (x : α) => x - a) '' uIcc b c = uIcc (b - a) (c - a)

theorem Set.image_neg_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] (a b : α) : Neg.neg '' uIcc a b = uIcc (-a) (-b)

theorem Set.abs_sub_le_of_uIcc_subset_uIcc {α : Type u_1} [LinearOrderedAddCommGroup α] {a b c d : α} (h : uIcc c d ⊆ 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} [LinearOrderedAddCommGroup α] {a b c : α} (h : c ∈ 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} [LinearOrderedAddCommGroup α] {a b c : α} (h : c ∈ 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} [LinearOrderedField α] (a : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) ⁻¹' Iio a = Iio (a / c)

@[simp]

theorem Set.preimage_mul_const_Ioi {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) ⁻¹' Ioi a = Ioi (a / c)

@[simp]

theorem Set.preimage_mul_const_Iic {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) ⁻¹' Iic a = Iic (a / c)

@[simp]

theorem Set.preimage_mul_const_Ici {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) ⁻¹' Ici a = Ici (a / c)

@[simp]

theorem Set.preimage_mul_const_Ioo {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

@[simp]

theorem Set.preimage_mul_const_Ioc {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c)

@[simp]

theorem Set.preimage_mul_const_Ico {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)

@[simp]

theorem Set.preimage_mul_const_Icc {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) ⁻¹' Icc a b = Icc (a / c) (b / c)

@[simp]

theorem Set.preimage_mul_const_Iio_of_neg {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : c < 0) : (fun (x : α) => x * c) ⁻¹' Iio a = Ioi (a / c)

@[simp]

theorem Set.preimage_mul_const_Ioi_of_neg {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : c < 0) : (fun (x : α) => x * c) ⁻¹' Ioi a = Iio (a / c)

@[simp]

theorem Set.preimage_mul_const_Iic_of_neg {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : c < 0) : (fun (x : α) => x * c) ⁻¹' Iic a = Ici (a / c)

@[simp]

theorem Set.preimage_mul_const_Ici_of_neg {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : c < 0) : (fun (x : α) => x * c) ⁻¹' Ici a = Iic (a / c)

@[simp]

theorem Set.preimage_mul_const_Ioo_of_neg {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : c < 0) : (fun (x : α) => x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c)

@[simp]

theorem Set.preimage_mul_const_Ioc_of_neg {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : c < 0) : (fun (x : α) => x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)

@[simp]

theorem Set.preimage_mul_const_Ico_of_neg {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : c < 0) : (fun (x : α) => x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)

@[simp]

theorem Set.preimage_mul_const_Icc_of_neg {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : c < 0) : (fun (x : α) => x * c) ⁻¹' Icc a b = Icc (b / c) (a / c)

@[simp]

theorem Set.preimage_const_mul_Iio {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : 0 < c) : (fun (x : α) => c * x) ⁻¹' Iio a = Iio (a / c)

@[simp]

theorem Set.preimage_const_mul_Ioi {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : 0 < c) : (fun (x : α) => c * x) ⁻¹' Ioi a = Ioi (a / c)

@[simp]

theorem Set.preimage_const_mul_Iic {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : 0 < c) : (fun (x : α) => c * x) ⁻¹' Iic a = Iic (a / c)

@[simp]

theorem Set.preimage_const_mul_Ici {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : 0 < c) : (fun (x : α) => c * x) ⁻¹' Ici a = Ici (a / c)

@[simp]

theorem Set.preimage_const_mul_Ioo {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => c * x) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

@[simp]

theorem Set.preimage_const_mul_Ioc {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => c * x) ⁻¹' Ioc a b = Ioc (a / c) (b / c)

@[simp]

theorem Set.preimage_const_mul_Ico {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => c * x) ⁻¹' Ico a b = Ico (a / c) (b / c)

@[simp]

theorem Set.preimage_const_mul_Icc {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => c * x) ⁻¹' Icc a b = Icc (a / c) (b / c)

@[simp]

theorem Set.preimage_const_mul_Iio_of_neg {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : c < 0) : (fun (x : α) => c * x) ⁻¹' Iio a = Ioi (a / c)

@[simp]

theorem Set.preimage_const_mul_Ioi_of_neg {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : c < 0) : (fun (x : α) => c * x) ⁻¹' Ioi a = Iio (a / c)

@[simp]

theorem Set.preimage_const_mul_Iic_of_neg {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : c < 0) : (fun (x : α) => c * x) ⁻¹' Iic a = Ici (a / c)

@[simp]

theorem Set.preimage_const_mul_Ici_of_neg {α : Type u_1} [LinearOrderedField α] (a : α) {c : α} (h : c < 0) : (fun (x : α) => c * x) ⁻¹' Ici a = Iic (a / c)

@[simp]

theorem Set.preimage_const_mul_Ioo_of_neg {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : c < 0) : (fun (x : α) => c * x) ⁻¹' Ioo a b = Ioo (b / c) (a / c)

@[simp]

theorem Set.preimage_const_mul_Ioc_of_neg {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : c < 0) : (fun (x : α) => c * x) ⁻¹' Ioc a b = Ico (b / c) (a / c)

@[simp]

theorem Set.preimage_const_mul_Ico_of_neg {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : c < 0) : (fun (x : α) => c * x) ⁻¹' Ico a b = Ioc (b / c) (a / c)

@[simp]

theorem Set.preimage_const_mul_Icc_of_neg {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : c < 0) : (fun (x : α) => c * x) ⁻¹' Icc a b = Icc (b / c) (a / c)

@[simp]

theorem Set.preimage_mul_const_uIcc {α : Type u_1} [LinearOrderedField α] {a : α} (ha : a ≠ 0) (b c : α) : (fun (x : α) => x * a) ⁻¹' uIcc b c = uIcc (b / a) (c / a)

@[simp]

theorem Set.preimage_const_mul_uIcc {α : Type u_1} [LinearOrderedField α] {a : α} (ha : a ≠ 0) (b c : α) : (fun (x : α) => a * x) ⁻¹' uIcc b c = uIcc (b / a) (c / a)

@[simp]

theorem Set.preimage_div_const_uIcc {α : Type u_1} [LinearOrderedField α] {a : α} (ha : a ≠ 0) (b c : α) : (fun (x : α) => x / a) ⁻¹' uIcc b c = uIcc (b * a) (c * a)

theorem Set.preimage_const_mul_Ioi_or_Iio {α : Type u_1} [LinearOrderedField α] {a : α} (hb : a ≠ 0) {U V : Set α} (hU : U ∈ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}) (hV : V = HMul.hMul a ⁻¹' U) : V ∈ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}

@[simp]

theorem Set.image_mul_const_uIcc {α : Type u_1} [LinearOrderedField α] (a b c : α) : (fun (x : α) => x * a) '' uIcc b c = uIcc (b * a) (c * a)

@[simp]

theorem Set.image_const_mul_uIcc {α : Type u_1} [LinearOrderedField α] (a b c : α) : (fun (x : α) => a * x) '' uIcc b c = uIcc (a * b) (a * c)

@[simp]

theorem Set.image_div_const_uIcc {α : Type u_1} [LinearOrderedField α] (a b c : α) : (fun (x : α) => x / a) '' uIcc b c = uIcc (b / a) (c / a)

theorem Set.image_mul_right_Icc' {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) '' Icc a b = Icc (a * c) (b * c)

theorem Set.image_mul_right_Icc {α : Type u_1} [LinearOrderedField α] {a b c : α} (hab : a ≤ b) (hc : 0 ≤ c) : (fun (x : α) => x * c) '' Icc a b = Icc (a * c) (b * c)

theorem Set.image_mul_left_Icc' {α : Type u_1} [LinearOrderedField α] {a : α} (h : 0 < a) (b c : α) : (fun (x : α) => a * x) '' Icc b c = Icc (a * b) (a * c)

theorem Set.image_mul_left_Icc {α : Type u_1} [LinearOrderedField α] {a b c : α} (ha : 0 ≤ a) (hbc : b ≤ c) : (fun (x : α) => a * x) '' Icc b c = Icc (a * b) (a * c)

theorem Set.image_mul_right_Ioo {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) '' Ioo a b = Ioo (a * c) (b * c)

theorem Set.image_mul_left_Ioo {α : Type u_1} [LinearOrderedField α] {a : α} (h : 0 < a) (b c : α) : (fun (x : α) => a * x) '' Ioo b c = Ioo (a * b) (a * c)

theorem Set.image_mul_right_Ico {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) '' Ico a b = Ico (a * c) (b * c)

theorem Set.image_mul_left_Ico {α : Type u_1} [LinearOrderedField α] {a : α} (h : 0 < a) (b c : α) : (fun (x : α) => a * x) '' Ico b c = Ico (a * b) (a * c)

theorem Set.image_mul_right_Ioc {α : Type u_1} [LinearOrderedField α] (a b : α) {c : α} (h : 0 < c) : (fun (x : α) => x * c) '' Ioc a b = Ioc (a * c) (b * c)

theorem Set.image_mul_left_Ioc {α : Type u_1} [LinearOrderedField α] {a : α} (h : 0 < a) (b c : α) : (fun (x : α) => a * x) '' Ioc b c = Ioc (a * b) (a * c)

theorem Set.inv_Ioo_0_left {α : Type u_1} [LinearOrderedField α] {a : α} (ha : 0 < a) : (Ioo 0 a)⁻¹ = Ioi a⁻¹

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

theorem Set.inv_Ioo_0_right {α : Type u_1} [LinearOrderedField α] {a : α} (ha : a < 0) : (Ioo a 0)⁻¹ = Iio a⁻¹

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

theorem Set.inv_Ioi₀ {α : Type u_1} [LinearOrderedField α] {a : α} (ha : 0 < a) : (Ioi a)⁻¹ = Ioo 0 a⁻¹

theorem Set.inv_Iio₀ {α : Type u_1} [LinearOrderedField α] {a : α} (ha : a < 0) : (Iio a)⁻¹ = Ioo a⁻¹ 0

theorem Set.image_const_mul_Ioi_zero {k : Type u_2} [LinearOrderedField k] {x : k} (hx : 0 < x) : (fun (y : k) => x * y) '' Ioi 0 = Ioi 0

Images under x ↦ a * x + b

@[simp]

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

@[simp]

theorem Set.image_affine_Ico {α : Type u_1} [LinearOrderedField α] {a : α} (h : 0 < a) (b c d : α) : (fun (x : α) => a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)

@[simp]

theorem Set.image_affine_Ioc {α : Type u_1} [LinearOrderedField α] {a : α} (h : 0 < a) (b c d : α) : (fun (x : α) => a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)

@[simp]

theorem Set.image_affine_Ioo {α : Type u_1} [LinearOrderedField α] {a : α} (h : 0 < a) (b c d : α) : (fun (x : α) => a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)