doc-next-gen

Mathlib.Algebra.Order.Group.Pointwise.Interval

Module docstring

{"# (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 ","### Preimages under x ↦ a + x ","### Preimages under x ↦ x + a ","### Preimages under x ↦ x - a ","### Preimages under x ↦ a - x ","### Images under x ↦ a + x ","### Images under x ↦ x + a ","### Images under x ↦ -x ","### Images under x ↦ a - x ","### Images under x ↦ x - a ","### Bijections ","### Commutative group with zero

The only reason why we need G₀ to be commutative in this section is that we write a / c, not c⁻¹ * a.

TODO: decide if we should reformulate the lemmas in terms of c⁻¹ * a instead of depending on commutativity. ","### Images under x ↦ a * x + b in a semifield ","### Multiplication and inverse in a field "}

Set.Icc_mul_Icc_subset' theorem
(a b c d : α) : Icc a b * Icc c d ⊆ Icc (a * c) (b * d)
Full source 
@[to_additive Icc_add_Icc_subset]
theorem Icc_mul_Icc_subset' (a b c d : α) : IccIcc a b * Icc c d ⊆ Icc (a * c) (b * d) := by
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_le_mul' hya hzc, mul_le_mul' hyb hzd⟩
Product of Closed Intervals is Contained in Closed Interval of Products
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ with multiplication, the product of the closed intervals $[a, b]$ and $[c, d]$ is contained in the closed interval $[a \cdot c, b \cdot d]$. In other words, if $x \in [a, b]$ and $y \in [c, d]$, then $x \cdot y \in [a \cdot c, b \cdot d]$.
Set.Iic_mul_Iic_subset' theorem
(a b : α) : Iic a * Iic b ⊆ Iic (a * b)
Full source 
@[to_additive Iic_add_Iic_subset]
theorem Iic_mul_Iic_subset' (a b : α) : IicIic a * Iic b ⊆ Iic (a * b) := by
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_le_mul' hya hzb
Product of Upper-Bounded Sets is Upper-Bounded by Product of Bounds
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with multiplication, the product of the sets $(-\infty, a]$ and $(-\infty, b]$ is contained in the set $(-\infty, a \cdot b]$. In other words, if $x \leq a$ and $y \leq b$, then $x \cdot y \leq a \cdot b$.
Set.Ici_mul_Ici_subset' theorem
(a b : α) : Ici a * Ici b ⊆ Ici (a * b)
Full source 
@[to_additive Ici_add_Ici_subset]
theorem Ici_mul_Ici_subset' (a b : α) : IciIci a * Ici b ⊆ Ici (a * b) := by
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_le_mul' hya hzb
Product of Closed-Infinite Intervals is Contained in Closed-Infinite Interval of Product
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with multiplication, the product of the closed-infinite intervals $[a, \infty)$ and $[b, \infty)$ is contained in the closed-infinite interval $[a \cdot b, \infty)$. In other words, if $x \in [a, \infty)$ and $y \in [b, \infty)$, then $x \cdot y \in [a \cdot b, \infty)$.
Set.Icc_mul_Ico_subset' theorem
(a b c d : α) : Icc a b * Ico c d ⊆ Ico (a * c) (b * d)
Full source 
@[to_additive Icc_add_Ico_subset]
theorem Icc_mul_Ico_subset' (a b c d : α) : IccIcc a b * Ico c d ⊆ Ico (a * c) (b * d) := by
  have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩
Product of Closed and Left-Closed Right-Open Intervals is Contained in Left-Closed Right-Open Interval
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ with multiplication, the product of the closed interval $[a, b]$ and the left-closed right-open interval $[c, d)$ is contained in the left-closed right-open interval $[a \cdot c, b \cdot d)$. In other words: $$[a, b] \cdot [c, d) \subseteq [a \cdot c, b \cdot d)$$
Set.Ico_mul_Icc_subset' theorem
(a b c d : α) : Ico a b * Icc c d ⊆ Ico (a * c) (b * d)
Full source 
@[to_additive Ico_add_Icc_subset]
theorem Ico_mul_Icc_subset' (a b c d : α) : IcoIco a b * Icc c d ⊆ Ico (a * c) (b * d) := by
  have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩
Product of Half-Open and Closed Intervals is Contained in Half-Open Interval
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ with multiplication, the product of the half-open interval $[a, b)$ and the closed interval $[c, d]$ is contained in the half-open interval $[a \cdot c, b \cdot d)$. In symbols: $$[a, b) \cdot [c, d] \subseteq [a \cdot c, b \cdot d)$$
Set.Ioc_mul_Ico_subset' theorem
(a b c d : α) : Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)
Full source 
@[to_additive Ioc_add_Ico_subset]
theorem Ioc_mul_Ico_subset' (a b c d : α) : IocIoc a b * Ico c d ⊆ Ioo (a * c) (b * d) := by
  have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_lt_mul_of_lt_of_le hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩
Product of $(a, b]$ and $[c, d)$ is contained in $(a \cdot c, b \cdot d)$
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ with multiplication, the product of the half-open interval $(a, b]$ and the half-open interval $[c, d)$ is contained in the open interval $(a \cdot c, b \cdot d)$. In other words, if $x \in (a, b]$ and $y \in [c, d)$, then $x \cdot y \in (a \cdot c, b \cdot d)$.
Set.Ico_mul_Ioc_subset' theorem
(a b c d : α) : Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d)
Full source 
@[to_additive Ico_add_Ioc_subset]
theorem Ico_mul_Ioc_subset' (a b c d : α) : IcoIco a b * Ioc c d ⊆ Ioo (a * c) (b * d) := by
  have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_lt_mul_of_le_of_lt hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩
Product of Half-Open Intervals is Contained in Open Interval
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ with multiplication, the product of the interval $[a, b) \times (c, d]$ is contained in the open interval $(a \cdot c, b \cdot d)$. In other words, if $x \in [a, b)$ and $y \in (c, d]$, then $x \cdot y \in (a \cdot c, b \cdot d)$.
Set.Iic_mul_Iio_subset' theorem
(a b : α) : Iic a * Iio b ⊆ Iio (a * b)
Full source 
@[to_additive Iic_add_Iio_subset]
theorem Iic_mul_Iio_subset' (a b : α) : IicIic a * Iio b ⊆ Iio (a * b) := by
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_lt_mul_of_le_of_lt hya hzb
Product of Closed and Open Unbounded Intervals is Contained in Open Unbounded Interval
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with multiplication, the product of the closed interval $(-\infty, a]$ and the open interval $(-\infty, b)$ is contained in the open interval $(-\infty, a \cdot b)$. In other words, if $x \leq a$ and $y < b$, then $x \cdot y < a \cdot b$.
Set.Iio_mul_Iic_subset' theorem
(a b : α) : Iio a * Iic b ⊆ Iio (a * b)
Full source 
@[to_additive Iio_add_Iic_subset]
theorem Iio_mul_Iic_subset' (a b : α) : IioIio a * Iic b ⊆ Iio (a * b) := by
  have := mulLeftMono_of_mulLeftStrictMono α
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_lt_mul_of_lt_of_le hya hzb
Product of Open and Closed Intervals is Contained in Open Interval
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with multiplication, the product of the open interval $(-\infty, a)$ and the closed interval $(-\infty, b]$ is contained in the open interval $(-\infty, a \cdot b)$. In other words, if $x < a$ and $y \leq b$, then $x \cdot y < a \cdot b$.
Set.Ioi_mul_Ici_subset' theorem
(a b : α) : Ioi a * Ici b ⊆ Ioi (a * b)
Full source 
@[to_additive Ioi_add_Ici_subset]
theorem Ioi_mul_Ici_subset' (a b : α) : IoiIoi a * Ici b ⊆ Ioi (a * b) := by
  have := mulLeftMono_of_mulLeftStrictMono α
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_lt_mul_of_lt_of_le hya hzb
Product of Right-Infinite Intervals: $(a, \infty) \cdot [b, \infty) \subseteq (a \cdot b, \infty)$
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with multiplication, the product of the open interval $(a, \infty)$ and the closed interval $[b, \infty)$ is contained in the open interval $(a \cdot b, \infty)$. In other words, if $x > a$ and $y \geq b$, then $x \cdot y > a \cdot b$.
Set.Ici_mul_Ioi_subset' theorem
(a b : α) : Ici a * Ioi b ⊆ Ioi (a * b)
Full source 
@[to_additive Ici_add_Ioi_subset]
theorem Ici_mul_Ioi_subset' (a b : α) : IciIci a * Ioi b ⊆ Ioi (a * b) := by
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_lt_mul_of_le_of_lt hya hzb
Product of Closed and Open Intervals is Contained in Open Interval: $[a, \infty) \cdot (b, \infty) \subseteq (a \cdot b, \infty)$
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with a multiplication operation, the product of the closed interval $[a, \infty)$ and the open interval $(b, \infty)$ is contained in the open interval $(a \cdot b, \infty)$. In other words, if $x \geq a$ and $y > b$, then $x \cdot y > a \cdot b$.
Set.smul_Icc theorem
(a b c : α) : a • Icc b c = Icc (a * b) (a * c)
Full source 
@[to_additive (attr := simp)]
lemma smul_Icc (a b c : α) : a • Icc b c = Icc (a * b) (a * c) := by
  ext x
  constructor
  · rintro ⟨y, ⟨hby, hyc⟩, rfl⟩
    exact ⟨mul_le_mul_left' hby _, mul_le_mul_left' hyc _⟩
  · rintro ⟨habx, hxac⟩
    obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le habx
    refine ⟨b * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
    rwa [mul_assoc, mul_le_mul_iff_left] at hxac
Scalar Multiplication Preserves Closed Interval: $a \cdot [b, c] = [a \cdot b, a \cdot c]$
Informal description
For any elements $a, b, c$ in a type $\alpha$ with suitable algebraic operations, the scalar multiplication of $a$ with the closed interval $[b, c]$ equals the closed interval $[a \cdot b, a \cdot c]$. In other words: $$ a \cdot [b, c] = [a \cdot b, a \cdot c] $$
Set.Icc_mul_Icc theorem
(hab : a ≤ b) (hcd : c ≤ d) : Icc a b * Icc c d = Icc (a * c) (b * d)
Full source 
@[to_additive]
lemma Icc_mul_Icc (hab : a ≤ b) (hcd : c ≤ d) : Icc a b * Icc c d = Icc (a * c) (b * d) := by
  refine (Icc_mul_Icc_subset' _ _ _ _).antisymm fun x ⟨hacx, hxbd⟩ ↦ ?_
  obtain hxbc | hbcx := le_total x (b * c)
  · obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hacx
    refine ⟨a * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, c, left_mem_Icc.2 hcd, mul_right_comm ..⟩
    rwa [mul_right_comm, mul_le_mul_iff_right] at hxbc
  · obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hbcx
    refine ⟨b, right_mem_Icc.2 hab, c * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
    rwa [mul_assoc, mul_le_mul_iff_left] at hxbd
Product of Closed Intervals Equals Closed Interval of Products
Informal description
For any elements $a, b, c, d$ in a type $\alpha$ with multiplication, if $a \leq b$ and $c \leq d$, then the product of the closed intervals $[a, b]$ and $[c, d]$ equals the closed interval $[a \cdot c, b \cdot d]$. In other words: $$ [a, b] \cdot [c, d] = [a \cdot c, b \cdot d] $$
Set.inv_Ici theorem
(a : α) : (Ici a)⁻¹ = Iic a⁻¹
Full source 
@[to_additive (attr := simp)] lemma inv_Ici (a : α) : (Ici a)⁻¹ = Iic a⁻¹ := ext fun _x ↦ le_inv'
Inverse of Upper Closed Interval Equals Lower Closed Interval of Inverse
Informal description
For any element $a$ in a linearly ordered commutative group with zero, the inverse of the closed interval $[a, \infty)$ is equal to the closed interval $(-\infty, a^{-1}]$.
Set.inv_Iic theorem
(a : α) : (Iic a)⁻¹ = Ici a⁻¹
Full source 
@[to_additive (attr := simp)] lemma inv_Iic (a : α) : (Iic a)⁻¹ = Ici a⁻¹ := ext fun _x ↦ inv_le'
Inversion Maps Lower Closed Interval to Upper Closed Interval
Informal description
For any element $a$ in a linearly ordered commutative group with zero $\alpha$, the preimage of the closed interval $(-\infty, a]$ under the inversion map $x \mapsto x^{-1}$ is the closed interval $[a^{-1}, \infty)$. In other words, $(Iic\, a)^{-1} = Ici\, a^{-1}$.
Set.inv_Ioi theorem
(a : α) : (Ioi a)⁻¹ = Iio a⁻¹
Full source 
@[to_additive (attr := simp)] lemma inv_Ioi (a : α) : (Ioi a)⁻¹ = Iio a⁻¹ := ext fun _x ↦ lt_inv'
Preimage of Right-Unbounded Open Interval under Inversion
Informal description
For any element $a$ in a linearly ordered commutative group with zero $\alpha$, the preimage of the open interval $(a, \infty)$ under the inversion operation $x \mapsto x^{-1}$ is equal to the open interval $(-\infty, a^{-1})$.
Set.inv_Iio theorem
(a : α) : (Iio a)⁻¹ = Ioi a⁻¹
Full source 
@[to_additive (attr := simp)] lemma inv_Iio (a : α) : (Iio a)⁻¹ = Ioi a⁻¹ := ext fun _x ↦ inv_lt'
Preimage of $(-\infty, a)$ under inversion is $(a^{-1}, \infty)$
Informal description
For any element $a$ in a linearly ordered commutative group with zero $\alpha$, the preimage of the open interval $(-\infty, a)$ under the inversion map $x \mapsto x^{-1}$ is equal to the open interval $(a^{-1}, \infty)$. In other words, $(Iio\, a)^{-1} = Ioi\, a^{-1}$.
Set.inv_Icc theorem
(a b : α) : (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹
Full source 
@[to_additive (attr := simp)]
lemma inv_Icc (a b : α) : (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹ := by simp [← Ici_inter_Iic, inter_comm]
Inverse of Closed Interval Equals Reversed Closed Interval of Inverses
Informal description
For any elements $a$ and $b$ in a linearly ordered commutative group with zero $\alpha$, the inverse of the closed interval $[a, b]$ is equal to the closed interval $[b^{-1}, a^{-1}]$. That is, $(Icc\, a\, b)^{-1} = Icc\, b^{-1}\, a^{-1}$.
Set.inv_Ico theorem
(a b : α) : (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹
Full source 
@[to_additive (attr := simp)]
lemma inv_Ico (a b : α) : (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹ := by
  simp [← Ici_inter_Iio, ← Ioi_inter_Iic, inter_comm]
Inverse of Half-Open Interval Equals Reversed Half-Open Interval of Inverses
Informal description
For any elements $a$ and $b$ in a linearly ordered commutative group with zero $\alpha$, the inverse of the half-open interval $[a, b)$ is equal to the half-open interval $(b^{-1}, a^{-1}]$. In other words, $(Ico\, a\, b)^{-1} = Ioc\, b^{-1}\, a^{-1}$.
Set.inv_Ioc theorem
(a b : α) : (Ioc a b)⁻¹ = Ico b⁻¹ a⁻¹
Full source 
@[to_additive (attr := simp)]
lemma inv_Ioc (a b : α) : (Ioc a b)⁻¹ = Ico b⁻¹ a⁻¹ := by
  simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
Inversion Maps Right-Open Left-Closed Interval to Left-Open Right-Closed Interval
Informal description
For any elements $a$ and $b$ in a linearly ordered commutative group with zero $\alpha$, the preimage of the right-open left-closed interval $(a, b]$ under the inversion map $x \mapsto x^{-1}$ is equal to the left-open right-closed interval $(b^{-1}, a^{-1}]$. In other words: $$(Ioc\, a\, b)^{-1} = Ico\, b^{-1}\, a^{-1}$$
Set.inv_Ioo theorem
(a b : α) : (Ioo a b)⁻¹ = Ioo b⁻¹ a⁻¹
Full source 
@[to_additive (attr := simp)]
lemma inv_Ioo (a b : α) : (Ioo a b)⁻¹ = Ioo b⁻¹ a⁻¹ := by simp [← Ioi_inter_Iio, inter_comm]
Inversion Maps Open Interval $(a, b)$ to $(b^{-1}, a^{-1})$
Informal description
For any elements $a$ and $b$ in a linearly ordered commutative group with zero $\alpha$, the preimage of the open interval $(a, b)$ under the inversion map $x \mapsto x^{-1}$ is equal to the open interval $(b^{-1}, a^{-1})$. In other words: $$(a, b)^{-1} = (b^{-1}, a^{-1})$$
Set.preimage_const_add_Ici theorem
: (fun x => a + x) ⁻¹' Ici b = Ici (b - a)
Full source 
@[simp]
theorem preimage_const_add_Ici : (fun x => a + x) ⁻¹' Ici b = Ici (b - a) :=
  ext fun _x => sub_le_iff_le_add'.symm
Preimage of Upper Closed Interval under Constant Addition
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with suitable algebraic structure, the preimage of the closed upper interval $[b, \infty)$ under the function $x \mapsto a + x$ is equal to the closed upper interval $[b - a, \infty)$. In other words: $$(x \mapsto a + x)^{-1}([b, \infty)) = [b - a, \infty)$$
Set.preimage_const_add_Ioi theorem
: (fun x => a + x) ⁻¹' Ioi b = Ioi (b - a)
Full source 
@[simp]
theorem preimage_const_add_Ioi : (fun x => a + x) ⁻¹' Ioi b = Ioi (b - a) :=
  ext fun _x => sub_lt_iff_lt_add'.symm
Preimage of Right-Infinite Open Interval under Constant Addition
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with addition structure, the preimage of the open interval $(b, \infty)$ under the function $x \mapsto a + x$ is equal to the open interval $(b - a, \infty)$. In symbols: $$(x \mapsto a + x)^{-1}((b, \infty)) = (b - a, \infty)$$
Set.preimage_const_add_Iic theorem
: (fun x => a + x) ⁻¹' Iic b = Iic (b - a)
Full source 
@[simp]
theorem preimage_const_add_Iic : (fun x => a + x) ⁻¹' Iic b = Iic (b - a) :=
  ext fun _x => le_sub_iff_add_le'.symm
Preimage of Closed Infinite Interval under Constant Addition
Informal description
For any real numbers $a$ and $b$, the preimage of the closed infinite interval $(-\infty, b]$ under the function $x \mapsto a + x$ is the closed infinite interval $(-\infty, b - a]$. In other words: $$\{x \mid a + x \leq b\} = (-\infty, b - a]$$
Set.preimage_const_add_Iio theorem
: (fun x => a + x) ⁻¹' Iio b = Iio (b - a)
Full source 
@[simp]
theorem preimage_const_add_Iio : (fun x => a + x) ⁻¹' Iio b = Iio (b - a) :=
  ext fun _x => lt_sub_iff_add_lt'.symm
Preimage of Open Interval under Addition by Constant
Informal description
For any real numbers $a$ and $b$, the preimage of the open interval $(-\infty, b)$ under the function $x \mapsto a + x$ is the open interval $(-\infty, b - a)$. In other words: $$\{x \mid a + x < b\} = \{x \mid x < b - a\}$$
Set.preimage_const_add_Icc theorem
: (fun x => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a)
Full source 
@[simp]
theorem preimage_const_add_Icc : (fun x => a + x) ⁻¹' Icc b c = Icc (b - a) (c - a) := by
  simp [← Ici_inter_Iic]
Preimage of Closed Interval under Constant Addition
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with suitable algebraic structure, the preimage of the closed interval $[b, c]$ under the function $x \mapsto a + x$ is equal to the closed interval $[b - a, c - a]$. In other words: $$(x \mapsto a + x)^{-1}([b, c]) = [b - a, c - a]$$
Set.preimage_const_add_Ico theorem
: (fun x => a + x) ⁻¹' Ico b c = Ico (b - a) (c - a)
Full source 
@[simp]
theorem preimage_const_add_Ico : (fun x => a + x) ⁻¹' Ico b c = Ico (b - a) (c - a) := by
  simp [← Ici_inter_Iio]
Preimage of Half-Open Interval under Constant Addition
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with suitable algebraic structure, the preimage of the half-open interval $[b, c)$ under the function $x \mapsto a + x$ is equal to the half-open interval $[b - a, c - a)$. In other words: $$(x \mapsto a + x)^{-1}([b, c)) = [b - a, c - a)$$
Set.preimage_const_add_Ioc theorem
: (fun x => a + x) ⁻¹' Ioc b c = Ioc (b - a) (c - a)
Full source 
@[simp]
theorem preimage_const_add_Ioc : (fun x => a + x) ⁻¹' Ioc b c = Ioc (b - a) (c - a) := by
  simp [← Ioi_inter_Iic]
Preimage of Right-Half-Open Interval under Constant Addition
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the half-open interval $(b, c]$ under the function $x \mapsto a + x$ is the half-open interval $(b - a, c - a]$. In other words: $$\{x \in \mathbb{R} \mid a + x \in (b, c]\} = (b - a, c - a]$$
Set.preimage_const_add_Ioo theorem
: (fun x => a + x) ⁻¹' Ioo b c = Ioo (b - a) (c - a)
Full source 
@[simp]
theorem preimage_const_add_Ioo : (fun x => a + x) ⁻¹' Ioo b c = Ioo (b - a) (c - a) := by
  simp [← Ioi_inter_Iio]
Preimage of Open Interval under Constant Addition
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the open interval $(b, c)$ under the function $x \mapsto a + x$ is the open interval $(b - a, c - a)$. In other words: $$\{x \in \mathbb{R} \mid a + x \in (b, c)\} = (b - a, c - a)$$
Set.preimage_add_const_Ici theorem
: (fun x => x + a) ⁻¹' Ici b = Ici (b - a)
Full source 
@[simp]
theorem preimage_add_const_Ici : (fun x => x + a) ⁻¹' Ici b = Ici (b - a) :=
  ext fun _x => sub_le_iff_le_add.symm
Preimage of Upper Closed Interval Under Right Addition
Informal description
For any real numbers $a$ and $b$, the preimage of the closed interval $[b, \infty)$ under the function $x \mapsto x + a$ is equal to the closed interval $[b - a, \infty)$. In other words: $$\{x \in \mathbb{R} \mid x + a \geq b\} = [b - a, \infty)$$
Set.preimage_add_const_Ioi theorem
: (fun x => x + a) ⁻¹' Ioi b = Ioi (b - a)
Full source 
@[simp]
theorem preimage_add_const_Ioi : (fun x => x + a) ⁻¹' Ioi b = Ioi (b - a) :=
  ext fun _x => sub_lt_iff_lt_add.symm
Preimage of Right-Infinite Open Interval under Right Addition Translation
Informal description
For any real numbers $a$ and $b$, the preimage of the open interval $(b, \infty)$ under the function $x \mapsto x + a$ is the open interval $(b - a, \infty)$. In other words: $$\{x \in \mathbb{R} \mid x + a > b\} = (b - a, \infty)$$
Set.preimage_add_const_Iic theorem
: (fun x => x + a) ⁻¹' Iic b = Iic (b - a)
Full source 
@[simp]
theorem preimage_add_const_Iic : (fun x => x + a) ⁻¹' Iic b = Iic (b - a) :=
  ext fun _x => le_sub_iff_add_le.symm
Preimage of closed ray under right translation
Informal description
For any real numbers $a$ and $b$, the preimage of the closed infinite interval $(-\infty, b]$ under the function $x \mapsto x + a$ is the closed infinite interval $(-\infty, b - a]$. In other words: $$\{x \mid x + a \leq b\} = (-\infty, b - a]$$
Set.preimage_add_const_Iio theorem
: (fun x => x + a) ⁻¹' Iio b = Iio (b - a)
Full source 
@[simp]
theorem preimage_add_const_Iio : (fun x => x + a) ⁻¹' Iio b = Iio (b - a) :=
  ext fun _x => lt_sub_iff_add_lt.symm
Preimage of Open Ray Under Right Translation
Informal description
For any real numbers $a$ and $b$, the preimage of the open interval $(-\infty, b)$ under the function $x \mapsto x + a$ is the open interval $(-\infty, b - a)$. In other words: $$\{x \mid x + a < b\} = (-\infty, b - a)$$
Set.preimage_add_const_Icc theorem
: (fun x => x + a) ⁻¹' Icc b c = Icc (b - a) (c - a)
Full source 
@[simp]
theorem preimage_add_const_Icc : (fun x => x + a) ⁻¹' Icc b c = Icc (b - a) (c - a) := by
  simp [← Ici_inter_Iic]
Preimage of Closed Interval Under Right Addition
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the closed interval $[b, c]$ under the function $x \mapsto x + a$ is the closed interval $[b - a, c - a]$. In other words: $$\{x \in \mathbb{R} \mid x + a \in [b, c]\} = [b - a, c - a]$$
Set.preimage_add_const_Ico theorem
: (fun x => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a)
Full source 
@[simp]
theorem preimage_add_const_Ico : (fun x => x + a) ⁻¹' Ico b c = Ico (b - a) (c - a) := by
  simp [← Ici_inter_Iio]
Preimage of Half-Open Interval Under Right Addition
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the half-open interval $[b, c)$ under the function $x \mapsto x + a$ is equal to the half-open interval $[b - a, c - a)$. In other words: $$\{x \in \mathbb{R} \mid x + a \in [b, c)\} = [b - a, c - a)$$
Set.preimage_add_const_Ioc theorem
: (fun x => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a)
Full source 
@[simp]
theorem preimage_add_const_Ioc : (fun x => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a) := by
  simp [← Ioi_inter_Iic]
Preimage of right-open interval under right translation: $\{x \mid x + a \in (b, c]\} = (b - a, c - a]$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the half-open interval $(b, c]$ under the function $x \mapsto x + a$ is the half-open interval $(b - a, c - a]$. In other words: $$\{x \in \mathbb{R} \mid x + a \in (b, c]\} = (b - a, c - a]$$
Set.preimage_add_const_Ioo theorem
: (fun x => x + a) ⁻¹' Ioo b c = Ioo (b - a) (c - a)
Full source 
@[simp]
theorem preimage_add_const_Ioo : (fun x => x + a) ⁻¹' Ioo b c = Ioo (b - a) (c - a) := by
  simp [← Ioi_inter_Iio]
Preimage of Open Interval under Right Translation: $(x + a)^{-1}((b, c)) = (b - a, c - a)$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the open interval $(b, c)$ under the function $x \mapsto x + a$ is the open interval $(b - a, c - a)$. In other words: $$\{x \in \mathbb{R} \mid b < x + a < c\} = (b - a, c - a)$$
Set.preimage_sub_const_Ici theorem
: (fun x => x - a) ⁻¹' Ici b = Ici (b + a)
Full source 
@[simp]
theorem preimage_sub_const_Ici : (fun x => x - a) ⁻¹' Ici b = Ici (b + a) := by
  simp [sub_eq_add_neg]
Preimage of Upper Closed Interval Under Left Subtraction
Informal description
For any real numbers $a$ and $b$, the preimage of the closed interval $[b, \infty)$ under the function $x \mapsto x - a$ is equal to the closed interval $[b + a, \infty)$. In other words: $$\{x \in \mathbb{R} \mid x - a \geq b\} = [b + a, \infty)$$
Set.preimage_sub_const_Ioi theorem
: (fun x => x - a) ⁻¹' Ioi b = Ioi (b + a)
Full source 
@[simp]
theorem preimage_sub_const_Ioi : (fun x => x - a) ⁻¹' Ioi b = Ioi (b + a) := by
  simp [sub_eq_add_neg]
Preimage of Right-Infinite Open Interval under Left Subtraction Translation
Informal description
For any real numbers $a$ and $b$, the preimage of the open interval $(b, \infty)$ under the function $x \mapsto x - a$ is the open interval $(b + a, \infty)$. In other words: $$\{x \in \mathbb{R} \mid x - a > b\} = (b + a, \infty)$$
Set.preimage_sub_const_Iic theorem
: (fun x => x - a) ⁻¹' Iic b = Iic (b + a)
Full source 
@[simp]
theorem preimage_sub_const_Iic : (fun x => x - a) ⁻¹' Iic b = Iic (b + a) := by
  simp [sub_eq_add_neg]
Preimage of closed ray under left translation by $a$
Informal description
For any real numbers $a$ and $b$, the preimage of the closed infinite interval $(-\infty, b]$ under the function $x \mapsto x - a$ is the closed infinite interval $(-\infty, b + a]$. In other words: $$\{x \mid x - a \leq b\} = (-\infty, b + a]$$
Set.preimage_sub_const_Iio theorem
: (fun x => x - a) ⁻¹' Iio b = Iio (b + a)
Full source 
@[simp]
theorem preimage_sub_const_Iio : (fun x => x - a) ⁻¹' Iio b = Iio (b + a) := by
  simp [sub_eq_add_neg]
Preimage of Open Ray Under Left Translation by $a$: $\{x \mid x - a < b\} = (-\infty, b + a)$
Informal description
For any real numbers $a$ and $b$, the preimage of the open interval $(-\infty, b)$ under the function $x \mapsto x - a$ is the open interval $(-\infty, b + a)$. In other words: $$\{x \mid x - a < b\} = (-\infty, b + a)$$
Set.preimage_sub_const_Icc theorem
: (fun x => x - a) ⁻¹' Icc b c = Icc (b + a) (c + a)
Full source 
@[simp]
theorem preimage_sub_const_Icc : (fun x => x - a) ⁻¹' Icc b c = Icc (b + a) (c + a) := by
  simp [sub_eq_add_neg]
Preimage of Closed Interval Under Left Translation by $a$: $\{x \mid x - a \in [b, c]\} = [b + a, c + a]$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the closed interval $[b, c]$ under the function $x \mapsto x - a$ is the closed interval $[b + a, c + a]$. In other words: $$\{x \in \mathbb{R} \mid x - a \in [b, c]\} = [b + a, c + a]$$
Set.preimage_sub_const_Ico theorem
: (fun x => x - a) ⁻¹' Ico b c = Ico (b + a) (c + a)
Full source 
@[simp]
theorem preimage_sub_const_Ico : (fun x => x - a) ⁻¹' Ico b c = Ico (b + a) (c + a) := by
  simp [sub_eq_add_neg]
Preimage of Half-Open Interval Under Left Translation: $\{x \mid x - a \in [b, c)\} = [b + a, c + a)$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the half-open interval $[b, c)$ under the function $x \mapsto x - a$ is the half-open interval $[b + a, c + a)$. In other words: $$\{x \in \mathbb{R} \mid x - a \in [b, c)\} = [b + a, c + a)$$
Set.preimage_sub_const_Ioc theorem
: (fun x => x - a) ⁻¹' Ioc b c = Ioc (b + a) (c + a)
Full source 
@[simp]
theorem preimage_sub_const_Ioc : (fun x => x - a) ⁻¹' Ioc b c = Ioc (b + a) (c + a) := by
  simp [sub_eq_add_neg]
Preimage of right-open interval under left translation: $\{x \mid x - a \in (b, c]\} = (b + a, c + a]$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the half-open interval $(b, c]$ under the function $x \mapsto x - a$ is the half-open interval $(b + a, c + a]$. In other words: $$\{x \in \mathbb{R} \mid x - a \in (b, c]\} = (b + a, c + a]$$
Set.preimage_sub_const_Ioo theorem
: (fun x => x - a) ⁻¹' Ioo b c = Ioo (b + a) (c + a)
Full source 
@[simp]
theorem preimage_sub_const_Ioo : (fun x => x - a) ⁻¹' Ioo b c = Ioo (b + a) (c + a) := by
  simp [sub_eq_add_neg]
Preimage of Open Interval under Left Translation: $(x - a)^{-1}((b, c)) = (b + a, c + a)$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the open interval $(b, c)$ under the function $x \mapsto x - a$ is the open interval $(b + a, c + a)$. In other words: $$\{x \in \mathbb{R} \mid b < x - a < c\} = (b + a, c + a)$$
Set.preimage_const_sub_Ici theorem
: (fun x => a - x) ⁻¹' Ici b = Iic (a - b)
Full source 
@[simp]
theorem preimage_const_sub_Ici : (fun x => a - x) ⁻¹' Ici b = Iic (a - b) :=
  ext fun _x => le_sub_comm
Preimage of $[b, \infty)$ under $x \mapsto a - x$ is $(-\infty, a - b]$
Informal description
For any real numbers $a$ and $b$, the preimage of the closed interval $[b, \infty)$ under the function $f(x) = a - x$ is equal to the closed interval $(-\infty, a - b]$. In other words: $$\{x \in \mathbb{R} \mid a - x \geq b\} = (-\infty, a - b]$$
Set.preimage_const_sub_Iic theorem
: (fun x => a - x) ⁻¹' Iic b = Ici (a - b)
Full source 
@[simp]
theorem preimage_const_sub_Iic : (fun x => a - x) ⁻¹' Iic b = Ici (a - b) :=
  ext fun _x => sub_le_comm
Preimage of $(-\infty, b]$ under $x \mapsto a - x$ is $[a - b, \infty)$
Informal description
For any real numbers $a$ and $b$, the preimage of the closed interval $(-\infty, b]$ under the function $x \mapsto a - x$ is the closed interval $[a - b, \infty)$. In other words: $$(x \mapsto a - x)^{-1}((-\infty, b]) = [a - b, \infty)$$
Set.preimage_const_sub_Ioi theorem
: (fun x => a - x) ⁻¹' Ioi b = Iio (a - b)
Full source 
@[simp]
theorem preimage_const_sub_Ioi : (fun x => a - x) ⁻¹' Ioi b = Iio (a - b) :=
  ext fun _x => lt_sub_comm
Preimage of $(b, \infty)$ under $x \mapsto a - x$ is $(-\infty, a - b)$
Informal description
For any real numbers $a$ and $b$, the preimage of the open interval $(b, \infty)$ under the function $f(x) = a - x$ is equal to the open interval $(-\infty, a - b)$. In other words: $$\{x \in \mathbb{R} \mid a - x > b\} = (-\infty, a - b)$$
Set.preimage_const_sub_Iio theorem
: (fun x => a - x) ⁻¹' Iio b = Ioi (a - b)
Full source 
@[simp]
theorem preimage_const_sub_Iio : (fun x => a - x) ⁻¹' Iio b = Ioi (a - b) :=
  ext fun _x => sub_lt_comm
Preimage of $(-\infty, b)$ under $x \mapsto a - x$ is $(a - b, \infty)$
Informal description
For any real numbers $a$ and $b$, the preimage of the open interval $(-\infty, b)$ under the function $x \mapsto a - x$ is the open interval $(a - b, \infty)$. In other words: $$(x \mapsto a - x)^{-1}((-\infty, b)) = (a - b, \infty)$$
Set.preimage_const_sub_Icc theorem
: (fun x => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b)
Full source 
@[simp]
theorem preimage_const_sub_Icc : (fun x => a - x) ⁻¹' Icc b c = Icc (a - c) (a - b) := by
  simp [← Ici_inter_Iic, inter_comm]
Preimage of $[b, c]$ under $x \mapsto a - x$ is $[a - c, a - b]$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the closed interval $[b, c]$ under the function $x \mapsto a - x$ is equal to the closed interval $[a - c, a - b]$. In other words: $$\{x \in \mathbb{R} \mid a - x \in [b, c]\} = [a - c, a - b]$$
Set.preimage_const_sub_Ico theorem
: (fun x => a - x) ⁻¹' Ico b c = Ioc (a - c) (a - b)
Full source 
@[simp]
theorem preimage_const_sub_Ico : (fun x => a - x) ⁻¹' Ico b c = Ioc (a - c) (a - b) := by
  simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
Preimage of $[b, c)$ under $x \mapsto a - x$ is $(a - c, a - b]$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the half-open interval $[b, c)$ under the function $x \mapsto a - x$ is equal to the half-open interval $(a - c, a - b]$. In other words: $$\{x \in \mathbb{R} \mid a - x \in [b, c)\} = (a - c, a - b]$$
Set.preimage_const_sub_Ioc theorem
: (fun x => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b)
Full source 
@[simp]
theorem preimage_const_sub_Ioc : (fun x => a - x) ⁻¹' Ioc b c = Ico (a - c) (a - b) := by
  simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]
Preimage of $(b, c]$ under $x \mapsto a - x$ is $[a - c, a - b)$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the half-open interval $(b, c]$ under the function $x \mapsto a - x$ is the half-open interval $[a - c, a - b)$. In other words: $$(x \mapsto a - x)^{-1}((b, c]) = [a - c, a - b)$$
Set.preimage_const_sub_Ioo theorem
: (fun x => a - x) ⁻¹' Ioo b c = Ioo (a - c) (a - b)
Full source 
@[simp]
theorem preimage_const_sub_Ioo : (fun x => a - x) ⁻¹' Ioo b c = Ioo (a - c) (a - b) := by
  simp [← Ioi_inter_Iio, inter_comm]
Preimage of $(b, c)$ under $x \mapsto a - x$ is $(a - c, a - b)$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the open interval $(b, c)$ under the function $x \mapsto a - x$ is the open interval $(a - c, a - b)$. In other words: $$\{x \in \mathbb{R} \mid a - x \in (b, c)\} = (a - c, a - b)$$
Set.image_const_add_Iic theorem
: (fun x => a + x) '' Iic b = Iic (a + b)
Full source 
theorem image_const_add_Iic : (fun x => a + x) '' Iic b = Iic (a + b) := by simp [add_comm]
Image of Closed Ray under Left Translation: $\{a + x \mid x \leq b\} = (-\infty, a + b]$
Informal description
For any real numbers $a$ and $b$, the image of the closed infinite interval $(-\infty, b]$ under the function $x \mapsto a + x$ is the closed infinite interval $(-\infty, a + b]$. In other words: $$\{a + x \mid x \leq b\} = (-\infty, a + b]$$
Set.image_const_add_Iio theorem
: (fun x => a + x) '' Iio b = Iio (a + b)
Full source 
theorem image_const_add_Iio : (fun x => a + x) '' Iio b = Iio (a + b) := by simp [add_comm]
Image of Open Ray Under Left Translation: $\{a + x \mid x < b\} = (-\infty, a + b)$
Informal description
For any real numbers $a$ and $b$, the image of the open interval $(-\infty, b)$ under the function $x \mapsto a + x$ is the open interval $(-\infty, a + b)$. In other words: $$\{a + x \mid x < b\} = (-\infty, a + b)$$
Set.image_add_const_Iic theorem
: (fun x => x + a) '' Iic b = Iic (b + a)
Full source 
theorem image_add_const_Iic : (fun x => x + a) '' Iic b = Iic (b + a) := by simp
Image of Closed Ray under Right Translation: $\{x + a \mid x \leq b\} = (-\infty, b + a]$
Informal description
For any real numbers $a$ and $b$, the image of the closed infinite interval $(-\infty, b]$ under the function $x \mapsto x + a$ is the closed infinite interval $(-\infty, b + a]$. In other words: $$\{x + a \mid x \leq b\} = (-\infty, b + a]$$
Set.image_add_const_Iio theorem
: (fun x => x + a) '' Iio b = Iio (b + a)
Full source 
theorem image_add_const_Iio : (fun x => x + a) '' Iio b = Iio (b + a) := by simp
Image of Open Ray Under Right Translation: $(x \mapsto x + a)((-\infty, b)) = (-\infty, b + a)$
Informal description
For any real numbers $a$ and $b$, the image of the open interval $(-\infty, b)$ under the function $x \mapsto x + a$ is the open interval $(-\infty, b + a)$. In other words: $$\{x + a \mid x < b\} = (-\infty, b + a)$$
Set.image_neg_Ici theorem
: Neg.neg '' Ici a = Iic (-a)
Full source 
theorem image_neg_Ici : Neg.negNeg.neg '' Ici a = Iic (-a) := by simp
Image of $[a, \infty)$ under negation equals $(-\infty, -a]$
Informal description
The image of the closed interval $[a, \infty)$ under the negation function $x \mapsto -x$ is equal to the closed interval $(-\infty, -a]$.
Set.image_neg_Iic theorem
: Neg.neg '' Iic a = Ici (-a)
Full source 
theorem image_neg_Iic : Neg.negNeg.neg '' Iic a = Ici (-a) := by simp
Negation maps $(-\infty, a]$ to $[-a, \infty)$
Informal description
The image of the closed interval $(-\infty, a]$ under the negation function $x \mapsto -x$ is the closed interval $[-a, \infty)$. In other words, $-(\infty, a] = [-a, \infty)$.
Set.image_neg_Ioi theorem
: Neg.neg '' Ioi a = Iio (-a)
Full source 
theorem image_neg_Ioi : Neg.negNeg.neg '' Ioi a = Iio (-a) := by simp
Negation Maps Open Right Interval to Open Left Interval
Informal description
The image of the open interval $(a, \infty)$ under the negation function $x \mapsto -x$ is the open interval $(-\infty, -a)$, i.e., $- (a, \infty) = (-\infty, -a)$.
Set.image_neg_Iio theorem
: Neg.neg '' Iio a = Ioi (-a)
Full source 
theorem image_neg_Iio : Neg.negNeg.neg '' Iio a = Ioi (-a) := by simp
Negation Maps Left-Infinite Open Interval to Right-Infinite Open Interval
Informal description
The image of the open interval $(-\infty, a)$ under the negation function $x \mapsto -x$ is the open interval $(-a, \infty)$. In other words, $- (-\infty, a) = (-a, \infty)$.
Set.image_neg_Icc theorem
: Neg.neg '' Icc a b = Icc (-b) (-a)
Full source 
theorem image_neg_Icc : Neg.negNeg.neg '' Icc a b = Icc (-b) (-a) := by simp
Negation Maps Closed Interval to Closed Interval: $- [a, b] = [-b, -a]$
Informal description
The image of the closed interval $[a, b]$ under the negation function $x \mapsto -x$ is the closed interval $[-b, -a]$, i.e., $- [a, b] = [-b, -a]$.
Set.image_neg_Ico theorem
: Neg.neg '' Ico a b = Ioc (-b) (-a)
Full source 
theorem image_neg_Ico : Neg.negNeg.neg '' Ico a b = Ioc (-b) (-a) := by simp
Negation Maps Half-Open Interval to Half-Open Interval: $- [a, b) = (-b, -a]$
Informal description
The image of the half-open interval $[a, b)$ under the negation function $x \mapsto -x$ is the half-open interval $(-b, -a]$. In other words, $- [a, b) = (-b, -a]$.
Set.image_neg_Ioc theorem
: Neg.neg '' Ioc a b = Ico (-b) (-a)
Full source 
theorem image_neg_Ioc : Neg.negNeg.neg '' Ioc a b = Ico (-b) (-a) := by simp
Negation Maps Half-Open Interval to Half-Open Interval: $- (a, b] = [-b, -a)$
Informal description
The image of the half-open interval $(a, b]$ under the negation function $x \mapsto -x$ is the half-open interval $[-b, -a)$. In other words, $- (a, b] = [-b, -a)$.
Set.image_neg_Ioo theorem
: Neg.neg '' Ioo a b = Ioo (-b) (-a)
Full source 
theorem image_neg_Ioo : Neg.negNeg.neg '' Ioo a b = Ioo (-b) (-a) := by simp
Negation Maps Open Interval to Open Interval: $- (a, b) = (-b, -a)$
Informal description
The image of the open interval $(a, b)$ under the negation function $x \mapsto -x$ is the open interval $(-b, -a)$. In other words, $- (a, b) = (-b, -a)$.
Set.image_const_sub_Ici theorem
: (fun x => a - x) '' Ici b = Iic (a - b)
Full source 
@[simp]
theorem image_const_sub_Ici : (fun x => a - x) '' Ici b = Iic (a - b) := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Right-Closed Ray under Linear Reflection: $a - [b, \infty) = (-\infty, a - b]$
Informal description
For any real numbers $a$ and $b$, the image of the closed infinite interval $[b, \infty)$ under the function $x \mapsto a - x$ is the closed infinite interval $(-\infty, a - b]$. In other words: $$\{a - x \mid x \geq b\} = (-\infty, a - b]$$
Set.image_const_sub_Iic theorem
: (fun x => a - x) '' Iic b = Ici (a - b)
Full source 
@[simp]
theorem image_const_sub_Iic : (fun x => a - x) '' Iic b = Ici (a - b) := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Lower Closed Interval Under Constant Subtraction: $(a - \cdot)((-\infty, b]) = [a - b, \infty)$
Informal description
For any real numbers $a$ and $b$, the image of the closed interval $(-\infty, b]$ under the function $x \mapsto a - x$ is equal to the closed interval $[a - b, \infty)$. In other words: $$\{a - x \mid x \leq b\} = [a - b, \infty)$$
Set.image_const_sub_Ioi theorem
: (fun x => a - x) '' Ioi b = Iio (a - b)
Full source 
@[simp]
theorem image_const_sub_Ioi : (fun x => a - x) '' Ioi b = Iio (a - b) := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Open Ray Under Reflection and Translation: $(a - x) \mid x > b = (-\infty, a - b)$
Informal description
For any real numbers $a$ and $b$, the image of the open interval $(b, \infty)$ under the function $x \mapsto a - x$ is the open interval $(-\infty, a - b)$. In other words: $$\{a - x \mid x > b\} = (-\infty, a - b)$$
Set.image_const_sub_Iio theorem
: (fun x => a - x) '' Iio b = Ioi (a - b)
Full source 
@[simp]
theorem image_const_sub_Iio : (fun x => a - x) '' Iio b = Ioi (a - b) := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Left-Infinite Open Interval under Linear Reflection and Translation
Informal description
For any real numbers $a$ and $b$, the image of the open interval $(-\infty, b)$ under the function $x \mapsto a - x$ is the open interval $(a - b, \infty)$. In other words: $$\{a - x \mid x < b\} = (a - b, \infty)$$
Set.image_const_sub_Icc theorem
: (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)
Full source 
@[simp]
theorem image_const_sub_Icc : (fun x => a - x) '' Icc b c = Icc (a - c) (a - b) := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Closed Interval Under Reflection and Translation: $a - [b, c] = [a - c, a - b]$
Informal description
For any real numbers $a$, $b$, and $c$, the image of the closed interval $[b, c]$ under the function $x \mapsto a - x$ is the closed interval $[a - c, a - b]$. In other words: $$\{a - x \mid x \in [b, c]\} = [a - c, a - b]$$
Set.image_const_sub_Ico theorem
: (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
Full source 
@[simp]
theorem image_const_sub_Ico : (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b) := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Half-Open Interval Under Reflection and Translation: $a - [b, c) = (a - c, a - b]$
Informal description
For any real numbers $a$, $b$, and $c$, the image of the left-closed right-open interval $[b, c)$ under the function $x \mapsto a - x$ is the left-open right-closed interval $(a - c, a - b]$. In other words: $$\{a - x \mid x \in [b, c)\} = (a - c, a - b]$$
Set.image_const_sub_Ioc theorem
: (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b)
Full source 
@[simp]
theorem image_const_sub_Ioc : (fun x => a - x) '' Ioc b c = Ico (a - c) (a - b) := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Left-Open Right-Closed Interval Under Reflection and Translation: $a - (b, c] = [a - c, a - b)$
Informal description
For any real numbers $a$, $b$, and $c$, the image of the left-open right-closed interval $(b, c]$ under the function $x \mapsto a - x$ is the left-closed right-open interval $[a - c, a - b)$. In other words: $$\{a - x \mid x \in (b, c]\} = [a - c, a - b)$$
Set.image_const_sub_Ioo theorem
: (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
Full source 
@[simp]
theorem image_const_sub_Ioo : (fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b) := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Open Interval under Reflection and Translation: $a - (b, c) = (a - c, a - b)$
Informal description
For any real numbers $a$, $b$, and $c$, the image of the open interval $(b, c)$ under the function $x \mapsto a - x$ is the open interval $(a - c, a - b)$. In other words: $$\{a - x \mid x \in (b, c)\} = (a - c, a - b)$$
Set.image_sub_const_Ici theorem
: (fun x => x - a) '' Ici b = Ici (b - a)
Full source 
@[simp]
theorem image_sub_const_Ici : (fun x => x - a) '' Ici b = Ici (b - a) := by simp [sub_eq_neg_add]
Image of Upper Closed Interval under Subtraction by Constant
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with suitable algebraic structure, the image of the closed upper interval $[b, \infty)$ under the function $x \mapsto x - a$ is equal to the closed upper interval $[b - a, \infty)$. In other words: $$\{x - a \mid x \in [b, \infty)\} = [b - a, \infty)$$
Set.image_sub_const_Iic theorem
: (fun x => x - a) '' Iic b = Iic (b - a)
Full source 
@[simp]
theorem image_sub_const_Iic : (fun x => x - a) '' Iic b = Iic (b - a) := by simp [sub_eq_neg_add]
Image of Closed Infinite Interval under Subtraction by Constant
Informal description
For any real numbers $a$ and $b$, the image of the closed infinite interval $(-\infty, b]$ under the function $x \mapsto x - a$ is the closed infinite interval $(-\infty, b - a]$. In other words: $$\{x - a \mid x \leq b\} = (-\infty, b - a]$$
Set.image_sub_const_Ioi theorem
: (fun x => x - a) '' Ioi b = Ioi (b - a)
Full source 
@[simp]
theorem image_sub_const_Ioi : (fun x => x - a) '' Ioi b = Ioi (b - a) := by simp [sub_eq_neg_add]
Image of Right-Infinite Open Interval under Subtraction by Constant
Informal description
For any elements $a$ and $b$ in a type $\alpha$ with subtraction structure, the image of the open interval $(b, \infty)$ under the function $x \mapsto x - a$ is equal to the open interval $(b - a, \infty)$. In symbols: $$\{x - a \mid x \in (b, \infty)\} = (b - a, \infty)$$
Set.image_sub_const_Iio theorem
: (fun x => x - a) '' Iio b = Iio (b - a)
Full source 
@[simp]
theorem image_sub_const_Iio : (fun x => x - a) '' Iio b = Iio (b - a) := by simp [sub_eq_neg_add]
Image of Open Interval under Subtraction by Constant: $\{x - a \mid x < b\} = (-\infty, b - a)$
Informal description
For any real numbers $a$ and $b$, the image of the open interval $(-\infty, b)$ under the function $x \mapsto x - a$ is the open interval $(-\infty, b - a)$. In other words: $$\{x - a \mid x < b\} = \{y \mid y < b - a\}$$
Set.image_sub_const_Icc theorem
: (fun x => x - a) '' Icc b c = Icc (b - a) (c - a)
Full source 
@[simp]
theorem image_sub_const_Icc : (fun x => x - a) '' Icc b c = Icc (b - a) (c - a) := by
  simp [sub_eq_neg_add]
Image of Closed Interval under Subtraction by Constant: $\{x - a \mid x \in [b, c]\} = [b - a, c - a]$
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with subtraction structure, the image of the closed interval $[b, c]$ under the function $x \mapsto x - a$ is equal to the closed interval $[b - a, c - a]$. In symbols: $$\{x - a \mid x \in [b, c]\} = [b - a, c - a]$$
Set.image_sub_const_Ico theorem
: (fun x => x - a) '' Ico b c = Ico (b - a) (c - a)
Full source 
@[simp]
theorem image_sub_const_Ico : (fun x => x - a) '' Ico b c = Ico (b - a) (c - a) := by
  simp [sub_eq_neg_add]
Image of Left-Closed Right-Open Interval under Subtraction by Constant: $\{x - a \mid x \in [b, c)\} = [b - a, c - a)$
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with subtraction structure, the image of the left-closed right-open interval $[b, c)$ under the function $x \mapsto x - a$ is equal to the left-closed right-open interval $[b - a, c - a)$. In symbols: $$\{x - a \mid x \in [b, c)\} = [b - a, c - a)$$
Set.image_sub_const_Ioc theorem
: (fun x => x - a) '' Ioc b c = Ioc (b - a) (c - a)
Full source 
@[simp]
theorem image_sub_const_Ioc : (fun x => x - a) '' Ioc b c = Ioc (b - a) (c - a) := by
  simp [sub_eq_neg_add]
Image of Left-Open Right-Closed Interval under Subtraction by Constant: $\{x - a \mid x \in (b, c]\} = (b - a, c - a]$
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with subtraction structure, the image of the left-open right-closed interval $(b, c]$ under the function $x \mapsto x - a$ is equal to the left-open right-closed interval $(b - a, c - a]$. In symbols: $$\{x - a \mid x \in (b, c]\} = (b - a, c - a]$$
Set.image_sub_const_Ioo theorem
: (fun x => x - a) '' Ioo b c = Ioo (b - a) (c - a)
Full source 
@[simp]
theorem image_sub_const_Ioo : (fun x => x - a) '' Ioo b c = Ioo (b - a) (c - a) := by
  simp [sub_eq_neg_add]
Image of Open Interval under Subtraction by Constant: $\{x - a \mid x \in (b, c)\} = (b - a, c - a)$
Informal description
For any real numbers $a$, $b$, and $c$, the image of the open interval $(b, c)$ under the function $x \mapsto x - a$ is the open interval $(b - a, c - a)$. In other words: $$\{x - a \mid x \in (b, c)\} = (b - a, c - a)$$
Set.Iic_add_bij theorem
: BijOn (· + a) (Iic b) (Iic (b + a))
Full source 
theorem Iic_add_bij : BijOn (· + a) (Iic b) (Iic (b + a)) :=
  image_add_const_Iic a b ▸ (add_left_injective _).injOn.bijOn_image
Bijection Between Closed Rays Under Right Translation: $(-\infty, b] \xrightarrow{x \mapsto x+a} (-\infty, b + a]$
Informal description
For any real numbers $a$ and $b$, the function $f(x) = x + a$ is a bijection from the closed infinite interval $(-\infty, b]$ to the closed infinite interval $(-\infty, b + a]$. In other words: 1. For every $x \in (-\infty, b]$, we have $f(x) \in (-\infty, b + a]$ 2. The function is injective on $(-\infty, b]$ 3. For every $y \in (-\infty, b + a]$, there exists $x \in (-\infty, b]$ such that $f(x) = y$
Set.Iio_add_bij theorem
: BijOn (· + a) (Iio b) (Iio (b + a))
Full source 
theorem Iio_add_bij : BijOn (· + a) (Iio b) (Iio (b + a)) :=
  image_add_const_Iio a b ▸ (add_left_injective _).injOn.bijOn_image
Bijection Between Open Rays Under Right Translation: $(-\infty, b) \xrightarrow{x \mapsto x+a} (-\infty, b + a)$
Informal description
For any real numbers $a$ and $b$, the function $f(x) = x + a$ is a bijection from the open interval $(-\infty, b)$ to the open interval $(-\infty, b + a)$. In other words: 1. For every $x \in (-\infty, b)$, we have $f(x) \in (-\infty, b + a)$ (maps into the target set) 2. The function is injective on $(-\infty, b)$ 3. For every $y \in (-\infty, b + a)$, there exists $x \in (-\infty, b)$ such that $f(x) = y$ (surjective onto the target set)
Set.inv_uIcc theorem
(a b : α) : [[a, b]]⁻¹ = [[a⁻¹, b⁻¹]]
Full source 
@[to_additive (attr := simp)]
lemma inv_uIcc (a b : α) : [[a, b]][[a, b]]⁻¹ = [[a⁻¹, b⁻¹]] := by
  simp only [uIcc, inv_Icc, inv_sup, inv_inf]
Inverse of Interval Equals Interval of Inverses: $[[a, b]]^{-1} = [[a^{-1}, b^{-1}]]$
Informal description
For any elements $a$ and $b$ in a linearly ordered commutative group with zero $\alpha$, the inverse of the interval $[[a, b]]$ is equal to the interval $[[a^{-1}, b^{-1}]]$. That is, $[[a, b]]^{-1} = [[a^{-1}, b^{-1}]]$.
Set.preimage_const_add_uIcc theorem
: (fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]
Full source 
@[simp]
theorem preimage_const_add_uIcc : (fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]] := by
  simp only [← Icc_min_max, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]
Preimage of Interval under Constant Addition: $(x \mapsto a + x)^{-1}([[b, c]]) = [[b - a, c - a]]$
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with suitable algebraic structure, the preimage of the interval $[[b, c]]$ under the function $x \mapsto a + x$ is equal to the interval $[[b - a, c - a]]$. In other words: $$(x \mapsto a + x)^{-1}([[b, c]]) = [[b - a, c - a]]$$
Set.preimage_neg_uIcc theorem
: -[[a, b]] = [[-a, -b]]
Full source 
@[deprecated neg_uIcc (since := "2024-11-23")]
theorem preimage_neg_uIcc : -[[a, b]] = [[-a, -b]] := by
  simp only [← Icc_min_max, neg_Icc, min_neg_neg, max_neg_neg]
Preimage of Closed Interval under Negation: $-[[a, b]] = [[-a, -b]]$
Informal description
For any real numbers $a$ and $b$, the preimage of the closed interval $[a, b]$ under the negation function $x \mapsto -x$ is equal to the closed interval $[-b, -a]$.
Set.preimage_sub_const_uIcc theorem
: (fun x => x - a) ⁻¹' [[b, c]] = [[b + a, c + a]]
Full source 
@[simp]
theorem preimage_sub_const_uIcc : (fun x => x - a) ⁻¹' [[b, c]] = [[b + a, c + a]] := by
  simp [sub_eq_add_neg]
Preimage of Closed Interval under $x \mapsto x - a$ is $[b + a, c + a]$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the closed interval $[b, c]$ under the function $x \mapsto x - a$ is equal to the closed interval $[b + a, c + a]$. In other words: $$\{x \in \mathbb{R} \mid x - a \in [b, c]\} = [b + a, c + a]$$
Set.preimage_const_sub_uIcc theorem
: (fun x => a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]
Full source 
@[simp]
theorem preimage_const_sub_uIcc : (fun x => a - x) ⁻¹' [[b, c]] = [[a - b, a - c]] := by
  simp_rw [← Icc_min_max, preimage_const_sub_Icc]
  simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg]
Preimage of Closed Interval under $x \mapsto a - x$ is $[a - c, a - b]$
Informal description
For any real numbers $a$, $b$, and $c$, the preimage of the closed interval $[b, c]$ under the function $x \mapsto a - x$ is equal to the closed interval $[a - c, a - b]$. In other words: $$\{x \in \mathbb{R} \mid a - x \in [b, c]\} = [a - c, a - b]$$
Set.image_const_add_uIcc theorem
: (fun x => a + x) '' [[b, c]] = [[a + b, a + c]]
Full source 
theorem image_const_add_uIcc : (fun x => a + x) '' [[b, c]] = [[a + b, a + c]] := by simp [add_comm]
Image of Interval under Left Addition: $(x \mapsto a + x)([b, c]) = [a + b, a + c]$
Informal description
For any real numbers $a$, $b$, and $c$, the image of the closed interval $[b, c]$ under the function $x \mapsto a + x$ is equal to the closed interval $[a + b, a + c]$. In other words: $$(x \mapsto a + x)([b, c]) = [a + b, a + c]$$
Set.image_add_const_uIcc theorem
: (fun x => x + a) '' [[b, c]] = [[b + a, c + a]]
Full source 
theorem image_add_const_uIcc : (fun x => x + a) '' [[b, c]] = [[b + a, c + a]] := by simp
Image of Interval under Right Addition: $(x \mapsto x + a)([[b, c]]) = [[b + a, c + a]]$
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with suitable algebraic structure, the image of the interval $[[b, c]]$ under the function $x \mapsto x + a$ is equal to the interval $[[b + a, c + a]]$. In other words: $$(x \mapsto x + a)([[b, c]]) = [[b + a, c + a]]$$
Set.image_const_sub_uIcc theorem
: (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
Full source 
@[simp]
theorem image_const_sub_uIcc : (fun x => a - x) '' [[b, c]] = [[a - b, a - c]] := by
  have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]
Image of Interval under Constant Minus Argument: $(x \mapsto a - x)([[b, c]]) = [[a - c, a - b]]$
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with suitable algebraic structure, the image of the interval $[[b, c]]$ under the function $x \mapsto a - x$ is equal to the interval $[[a - c, a - b]]$. In other words: $$(x \mapsto a - x)([[b, c]]) = [[a - c, a - b]]$$
Set.image_sub_const_uIcc theorem
: (fun x => x - a) '' [[b, c]] = [[b - a, c - a]]
Full source 
@[simp]
theorem image_sub_const_uIcc : (fun x => x - a) '' [[b, c]] = [[b - a, c - a]] := by
  simp [sub_eq_add_neg, add_comm]
Image of Interval under Subtraction: $(x \mapsto x - a)([[b, c]]) = [[b - a, c - a]]$
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with suitable algebraic structure, the image of the interval $[[b, c]]$ under the function $x \mapsto x - a$ is equal to the interval $[[b - a, c - a]]$. In other words: $$(x \mapsto x - a)([[b, c]]) = [[b - a, c - a]]$$
Set.image_neg_uIcc theorem
: Neg.neg '' [[a, b]] = [[-a, -b]]
Full source 
theorem image_neg_uIcc : Neg.negNeg.neg '' [[a, b]] = [[-a, -b]] := by simp
Negation of Interval: $-([a, b]) = [-b, -a]$
Informal description
The image of the closed interval $[a, b]$ under the negation function $x \mapsto -x$ is the closed interval $[-b, -a]$.
Set.abs_sub_le_of_uIcc_subset_uIcc theorem
(h : [[c, d]] ⊆ [[a, b]]) : |d - c| ≤ |b - a|
Full source 
/-- 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 abs_sub_le_of_uIcc_subset_uIcc (h : [[c, d]][[c, d]] ⊆ [[a, b]]) : |d - c| ≤ |b - a| := by
  rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs]
  rw [uIcc_subset_uIcc_iff_le] at h
  exact sub_le_sub h.2 h.1
Distance Inequality for Subintervals: $|d - c| \leq |b - a|$ when $[c,d] \subseteq [a,b]$
Informal description
If the interval $[c, d]$ is contained in the interval $[a, b]$, then the distance between $c$ and $d$ is less than or equal to the distance between $a$ and $b$, i.e., $|d - c| \leq |b - a|$.
Set.abs_sub_left_of_mem_uIcc theorem
(h : c ∈ [[a, b]]) : |c - a| ≤ |b - a|
Full source 
/-- If `c ∈ [a, b]`, then the distance between `a` and `c` is less than or equal to
that of `a` and `b` -/
theorem abs_sub_left_of_mem_uIcc (h : c ∈ [[a, b]]) : |c - a| ≤ |b - a| :=
  abs_sub_le_of_uIcc_subset_uIcc <| uIcc_subset_uIcc_left h
Distance Bound for Left Endpoint: $|c - a| \leq |b - a|$ when $c \in [a, b]$
Informal description
For any real numbers $a$, $b$, and $c$ such that $c$ belongs to the interval $[a, b]$, the distance between $c$ and $a$ is less than or equal to the distance between $b$ and $a$, i.e., $|c - a| \leq |b - a|$.
Set.abs_sub_right_of_mem_uIcc theorem
(h : c ∈ [[a, b]]) : |b - c| ≤ |b - a|
Full source 
/-- If `x ∈ [a, b]`, then the distance between `c` and `b` is less than or equal to
that of `a` and `b` -/
theorem abs_sub_right_of_mem_uIcc (h : c ∈ [[a, b]]) : |b - c| ≤ |b - a| :=
  abs_sub_le_of_uIcc_subset_uIcc <| uIcc_subset_uIcc_right h
Distance from Interval Endpoint: $|b - c| \leq |b - a|$ when $c \in [a, b]$
Informal description
For any real number $c$ in the interval $[a, b]$, the distance between $b$ and $c$ is less than or equal to the distance between $b$ and $a$, i.e., $|b - c| \leq |b - a|$.
Set.preimage_mul_const_Iic theorem
(a : G₀) (h : 0 < c) : (· * c) ⁻¹' Iic a = Iic (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Iic (a : G₀) (h : 0 < c) : (· * c) ⁻¹' Iic a = Iic (a / c) := by
  simpa only [division_def] using (OrderIso.mulRight₀ c h).preimage_Iic a
Preimage of $Iic$ under right multiplication equals $Iic$ of quotient
Informal description
Let $G₀$ be a commutative group with zero, $a \in G₀$, and $c \in G₀$ with $0 < c$. The preimage of the closed infinite interval $(-\infty, a]$ under the function $x \mapsto x \cdot c$ is equal to the closed infinite interval $(-\infty, a/c]$.
Set.preimage_mul_const_Ici theorem
(a : G₀) (h : 0 < c) : (· * c) ⁻¹' Ici a = Ici (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Ici (a : G₀) (h : 0 < c) : (· * c) ⁻¹' Ici a = Ici (a / c) := by
  simpa only [division_def] using (OrderIso.mulRight₀ c h).preimage_Ici a
Preimage of $[a, \infty)$ under right multiplication by $c$ is $\left[\frac{a}{c}, \infty\right)$ for $c > 0$
Informal description
Let $G₀$ be a commutative group with zero. For any elements $a, c \in G₀$ with $c > 0$, the preimage of the closed interval $[a, \infty)$ under the function $x \mapsto x \cdot c$ is equal to the closed interval $\left[\frac{a}{c}, \infty\right)$.
Set.preimage_mul_const_Ioi theorem
(a : G₀) (h : 0 < c) : (· * c) ⁻¹' Ioi a = Ioi (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Ioi (a : G₀) (h : 0 < c) : (· * c) ⁻¹' Ioi a = Ioi (a / c) := by
  simpa only [division_def] using (OrderIso.mulRight₀ c h).preimage_Ioi a
Preimage of Right-Unbounded Open Interval under Right Multiplication by Positive Scalar
Informal description
For any elements $a$ and $c$ in a commutative group with zero $G_0$, if $c > 0$, then the preimage of the open interval $(a, \infty)$ under the function $x \mapsto x \cdot c$ is equal to the open interval $(a/c, \infty)$. In mathematical notation: $$(x \mapsto x \cdot c)^{-1}\big((a, \infty)\big) = \left(\frac{a}{c}, \infty\right)$$
Set.preimage_mul_const_Iio theorem
(a : G₀) (h : 0 < c) : (· * c) ⁻¹' Iio a = Iio (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Iio (a : G₀) (h : 0 < c) : (· * c) ⁻¹' Iio a = Iio (a / c) := by
  simpa only [division_def] using (OrderIso.mulRight₀ c h).preimage_Iio a
Preimage of Left-Infinite Open Interval under Right Multiplication by Positive Constant
Informal description
Let $G₀$ be a commutative group with zero, and let $c$ be a positive element of $G₀$. For any $a \in G₀$, the preimage of the open left-infinite interval $(-\infty, a)$ under the function $x \mapsto x * c$ is equal to the open left-infinite interval $(-\infty, a/c)$. In other words: $$(x \mapsto x * c)^{-1}((-\infty, a)) = (-\infty, a/c)$$
Set.preimage_mul_const_Icc theorem
(a b : G₀) (h : 0 < c) : (· * c) ⁻¹' Icc a b = Icc (a / c) (b / c)
Full source 
@[simp]
theorem preimage_mul_const_Icc (a b : G₀) (h : 0 < c) :
    (· * c) ⁻¹' Icc a b = Icc (a / c) (b / c) := by simp [← Ici_inter_Iic, h]
Preimage of Closed Interval under Right Multiplication by Positive Scalar
Informal description
Let $G₀$ be a commutative group with zero, and let $a, b, c \in G₀$ with $c > 0$. The preimage of the closed interval $[a, b]$ under the function $x \mapsto x \cdot c$ is equal to the closed interval $\left[\frac{a}{c}, \frac{b}{c}\right]$. In mathematical notation: $$(x \mapsto x \cdot c)^{-1}\big([a, b]\big) = \left[\frac{a}{c}, \frac{b}{c}\right]$$
Set.preimage_mul_const_Ioo theorem
(a b : G₀) (h : 0 < c) : (fun x => x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c)
Full source 
@[simp]
theorem preimage_mul_const_Ioo (a b : G₀) (h : 0 < c) :
    (fun x => x * c) ⁻¹' Ioo a b = Ioo (a / c) (b / c) := by simp [← Ioi_inter_Iio, h]
Preimage of Open Interval under Right Multiplication by Positive Scalar
Informal description
Let $G₀$ be a commutative group with zero, and let $c$ be a positive element of $G₀$. For any $a, b \in G₀$, the preimage of the open interval $(a, b)$ under the function $x \mapsto x \cdot c$ is equal to the open interval $(a/c, b/c)$. In mathematical notation: $$(x \mapsto x \cdot c)^{-1}\big((a, b)\big) = \left(\frac{a}{c}, \frac{b}{c}\right)$$
Set.preimage_mul_const_Ioc theorem
(a b : G₀) (h : 0 < c) : (fun x => x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c)
Full source 
@[simp]
theorem preimage_mul_const_Ioc (a b : G₀) (h : 0 < c) :
    (fun x => x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c) := by simp [← Ioi_inter_Iic, h]
Preimage of Right-Half-Open Interval under Right Multiplication by Positive Scalar
Informal description
Let $G₀$ be a commutative group with zero, and let $a, b, c \in G₀$ with $c > 0$. The preimage of the half-open interval $(a, b]$ under the function $x \mapsto x \cdot c$ is equal to the half-open interval $(a/c, b/c]$. In mathematical notation: $$(x \mapsto x \cdot c)^{-1}\big((a, b]\big) = \left(\frac{a}{c}, \frac{b}{c}\right]$$
Set.preimage_mul_const_Ico theorem
(a b : G₀) (h : 0 < c) : (fun x => x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)
Full source 
@[simp]
theorem preimage_mul_const_Ico (a b : G₀) (h : 0 < c) :
    (fun x => x * c) ⁻¹' Ico a b = Ico (a / c) (b / c) := by simp [← Ici_inter_Iio, h]
Preimage of $[a, b)$ under right multiplication by $c > 0$ is $\left[\frac{a}{c}, \frac{b}{c}\right)$
Informal description
Let $G₀$ be a commutative group with zero. For any elements $a, b \in G₀$ and any positive element $c \in G₀$, the preimage of the half-open interval $[a, b)$ under the function $x \mapsto x \cdot c$ is equal to the half-open interval $\left[\frac{a}{c}, \frac{b}{c}\right)$. In other words: $$(x \mapsto x \cdot c)^{-1}([a, b)) = \left[\frac{a}{c}, \frac{b}{c}\right)$$
Set.image_mul_right_Icc' theorem
(a b : G₀) (h : 0 < c) : (· * c) '' Icc a b = Icc (a * c) (b * c)
Full source 
theorem image_mul_right_Icc' (a b : G₀) (h : 0 < c) :
    (· * c) '' Icc a b = Icc (a * c) (b * c) :=
  (OrderIso.mulRight₀ c h).image_Icc a b
Image of Closed Interval under Right Multiplication by Positive Element in Commutative Group with Zero
Informal description
For any elements $a, b$ in a commutative group with zero $G₀$ and any positive element $c \in G₀$, the image of the closed interval $[a, b]$ under right multiplication by $c$ is equal to the closed interval $[a \cdot c, b \cdot c]$. That is, $$ \{x \cdot c \mid x \in [a, b]\} = [a \cdot c, b \cdot c]. $$
Set.image_mul_right_Icc theorem
(hab : a ≤ b) (hc : 0 ≤ c) : (· * c) '' Icc a b = Icc (a * c) (b * c)
Full source 
theorem image_mul_right_Icc (hab : a ≤ b) (hc : 0 ≤ c) :
    (· * c) '' Icc a b = Icc (a * c) (b * c) := by
  cases eq_or_lt_of_le hc
  · subst c
    simp [(nonempty_Icc.2 hab).image_const]
  exact image_mul_right_Icc' a b ‹0 < c›
Image of Closed Interval under Right Multiplication by Nonnegative Element: $[a, b] \cdot c = [a \cdot c, b \cdot c]$
Informal description
For any elements $a, b$ in a commutative group with zero $G₀$ such that $a \leq b$, and any nonnegative element $c \geq 0$, the image of the closed interval $[a, b]$ under right multiplication by $c$ is equal to the closed interval $[a \cdot c, b \cdot c]$. That is, $$ \{x \cdot c \mid x \in [a, b]\} = [a \cdot c, b \cdot c]. $$
Set.image_mul_right_Ioo theorem
(a b : G₀) (h : 0 < c) : (fun x => x * c) '' Ioo a b = Ioo (a * c) (b * c)
Full source 
theorem image_mul_right_Ioo (a b : G₀) (h : 0 < c) :
    (fun x => x * c) '' Ioo a b = Ioo (a * c) (b * c) :=
  (OrderIso.mulRight₀ c h).image_Ioo a b
Image of Open Interval under Right Multiplication by Positive Element
Informal description
For any elements $a, b, c$ in a commutative group with zero $G₀$ where $0 < c$, the image of the open interval $(a, b)$ under the right multiplication map $x \mapsto x \cdot c$ is equal to the open interval $(a \cdot c, b \cdot c)$. In symbols: $$\{x \cdot c \mid x \in (a, b)\} = (a \cdot c, b \cdot c)$$
Set.image_mul_right_Ico theorem
(a b : G₀) (h : 0 < c) : (fun x => x * c) '' Ico a b = Ico (a * c) (b * c)
Full source 
theorem image_mul_right_Ico (a b : G₀) (h : 0 < c) :
    (fun x => x * c) '' Ico a b = Ico (a * c) (b * c) :=
  (OrderIso.mulRight₀ c h).image_Ico a b
Right multiplication preserves left-closed right-open intervals in a commutative group with zero
Informal description
For any elements $a, b$ in a commutative group with zero $G₀$ and any positive element $c > 0$, the image of the left-closed right-open interval $[a, b)$ under the right multiplication map $x \mapsto x \cdot c$ is the left-closed right-open interval $[a \cdot c, b \cdot c)$.
Set.image_mul_right_Ioc theorem
(a b : G₀) (h : 0 < c) : (fun x => x * c) '' Ioc a b = Ioc (a * c) (b * c)
Full source 
theorem image_mul_right_Ioc (a b : G₀) (h : 0 < c) :
    (fun x => x * c) '' Ioc a b = Ioc (a * c) (b * c) :=
  (OrderIso.mulRight₀ c h).image_Ioc a b
Image of Right-Open Interval under Right Multiplication by Positive Element
Informal description
Let $G₀$ be a commutative group with zero. For any elements $a, b, c \in G₀$ with $0 < c$, the image of the right-open, left-closed interval $(a, b]$ under the function $x \mapsto x \cdot c$ equals the right-open, left-closed interval $(a \cdot c, b \cdot c]$. In mathematical notation: $$\{x \cdot c \mid x \in (a, b]\} = (a \cdot c, b \cdot c]$$
Set.image_mul_left_Ici theorem
(h : 0 < a) (b : G₀) : (a * ·) '' Ici b = Ici (a * b)
Full source 
theorem image_mul_left_Ici (h : 0 < a) (b : G₀) : (a * ·) '' Ici b = Ici (a * b) :=
  (OrderIso.mulLeft₀ a h).image_Ici b
Image of Closed Right-Infinite Interval under Left Multiplication by Positive Element
Informal description
For any positive element $a > 0$ in a commutative group with zero $G₀$ and any element $b \in G₀$, the image of the closed right-infinite interval $[b, \infty)$ under the left multiplication map $x \mapsto a \cdot x$ is the closed right-infinite interval $[a \cdot b, \infty)$.
Set.image_mul_left_Iic theorem
(h : 0 < a) (b : G₀) : (a * ·) '' Iic b = Iic (a * b)
Full source 
theorem image_mul_left_Iic (h : 0 < a) (b : G₀) : (a * ·) '' Iic b = Iic (a * b) :=
  (OrderIso.mulLeft₀ a h).image_Iic b
Image of Left-Infinite Closed Interval under Left Multiplication by Positive Element
Informal description
Let $G₀$ be a commutative group with zero. For any elements $a, b \in G₀$ with $0 < a$, the image of the left-infinite closed interval $(-\infty, b]$ under the function $x \mapsto a \cdot x$ equals the left-infinite closed interval $(-\infty, a \cdot b]$. In mathematical notation: $$\{a \cdot x \mid x \leq b\} = \{y \mid y \leq a \cdot b\}$$
Set.image_mul_left_Ioi theorem
(h : 0 < a) (b : G₀) : (a * ·) '' Ioi b = Ioi (a * b)
Full source 
theorem image_mul_left_Ioi (h : 0 < a) (b : G₀) : (a * ·) '' Ioi b = Ioi (a * b) :=
  (OrderIso.mulLeft₀ a h).image_Ioi b
Image of Right-Infinite Open Interval under Left Multiplication by Positive Element
Informal description
Let $G₀$ be a commutative group with zero and let $a, b \in G₀$ with $0 < a$. The image of the open right-infinite interval $(b, \infty)$ under the function $x \mapsto a \cdot x$ is the open right-infinite interval $(a \cdot b, \infty)$. In other words: $$\{a \cdot x \mid x > b\} = \{y \mid y > a \cdot b\}$$
Set.image_mul_left_Iio theorem
(h : 0 < a) (b : G₀) : (a * ·) '' Iio b = Iio (a * b)
Full source 
theorem image_mul_left_Iio (h : 0 < a) (b : G₀) : (a * ·) '' Iio b = Iio (a * b) :=
  (OrderIso.mulLeft₀ a h).image_Iio b
Image of Left-Infinite Open Interval under Left Multiplication by Positive Element
Informal description
Let $G₀$ be a commutative group with zero and let $a, b \in G₀$ with $0 < a$. The image of the left-infinite open interval $(-\infty, b)$ under the function $x \mapsto a \cdot x$ is the left-infinite open interval $(-\infty, a \cdot b)$. In other words: $$\{a \cdot x \mid x < b\} = \{y \mid y < a \cdot b\}$$
Set.image_mul_left_Icc' theorem
(h : 0 < a) (b c : G₀) : (a * ·) '' Icc b c = Icc (a * b) (a * c)
Full source 
theorem image_mul_left_Icc' (h : 0 < a) (b c : G₀) :
    (a * ·) '' Icc b c = Icc (a * b) (a * c) :=
  (OrderIso.mulLeft₀ a h).image_Icc b c
Image of Closed Interval under Left Multiplication by Positive Element
Informal description
Let $G₀$ be a commutative group with zero and let $a, b, c \in G₀$ with $0 < a$. The image of the closed interval $[b, c]$ under the function $x \mapsto a \cdot x$ is the closed interval $[a \cdot b, a \cdot c]$. In other words: $$\{a \cdot x \mid x \in [b, c]\} = [a \cdot b, a \cdot c]$$
Set.image_mul_left_Icc theorem
(ha : 0 ≤ a) (hbc : b ≤ c) : (a * ·) '' Icc b c = Icc (a * b) (a * c)
Full source 
theorem image_mul_left_Icc (ha : 0 ≤ a) (hbc : b ≤ c) :
    (a * ·) '' Icc b c = Icc (a * b) (a * c) := by
  rcases ha.eq_or_lt with rfl | ha
  · simp [(nonempty_Icc.2 hbc).image_const]
  · exact image_mul_left_Icc' ha b c
Image of Closed Interval under Left Multiplication by Nonnegative Element
Informal description
Let $G₀$ be a commutative group with zero, and let $a, b, c \in G₀$ with $0 \leq a$ and $b \leq c$. The image of the closed interval $[b, c]$ under the function $x \mapsto a \cdot x$ is the closed interval $[a \cdot b, a \cdot c]$. In other words: $$\{a \cdot x \mid x \in [b, c]\} = [a \cdot b, a \cdot c]$$
Set.image_mul_left_Ioo theorem
(h : 0 < a) (b c : G₀) : (a * ·) '' Ioo b c = Ioo (a * b) (a * c)
Full source 
theorem image_mul_left_Ioo (h : 0 < a) (b c : G₀) : (a * ·) '' Ioo b c = Ioo (a * b) (a * c) :=
  (OrderIso.mulLeft₀ a h).image_Ioo b c
Image of Open Interval under Left Multiplication by a Positive Element
Informal description
Let $G₀$ be a commutative group with zero. For any positive element $a \in G₀$ (i.e., $0 < a$) and any elements $b, c \in G₀$, the image of the open interval $(b, c)$ under the left multiplication map $x \mapsto a \cdot x$ is equal to the open interval $(a \cdot b, a \cdot c)$.
Set.image_mul_left_Ico theorem
(h : 0 < a) (b c : G₀) : (a * ·) '' Ico b c = Ico (a * b) (a * c)
Full source 
theorem image_mul_left_Ico (h : 0 < a) (b c : G₀) :
    (a * ·) '' Ico b c = Ico (a * b) (a * c) :=
  (OrderIso.mulLeft₀ a h).image_Ico b c
Image of Left-Closed Right-Open Interval under Left Multiplication by a Positive Element
Informal description
For any positive element $a$ in a commutative group with zero $G₀$, and any elements $b, c \in G₀$, the image of the left-closed right-open interval $[b, c)$ under the left multiplication map $x \mapsto a \cdot x$ is equal to the left-closed right-open interval $[a \cdot b, a \cdot c)$.
Set.image_mul_left_Ioc theorem
(h : 0 < a) (b c : G₀) : (a * ·) '' Ioc b c = Ioc (a * b) (a * c)
Full source 
theorem image_mul_left_Ioc (h : 0 < a) (b c : G₀) :
    (a * ·) '' Ioc b c = Ioc (a * b) (a * c) :=
  (OrderIso.mulLeft₀ a h).image_Ioc b c
Image of Left-Open Right-Closed Interval under Left Multiplication by a Positive Element
Informal description
Let $G₀$ be a commutative group with zero. For any positive element $a \in G₀$ (i.e., $0 < a$) and any elements $b, c \in G₀$, the image of the left-open right-closed interval $Ioc(b, c)$ under the function $x \mapsto a \cdot x$ is equal to the left-open right-closed interval $Ioc(a \cdot b, a \cdot c)$.
Set.image_const_mul_Ioi_zero theorem
(ha : 0 < a) : (a * ·) '' Ioi 0 = Ioi 0
Full source 
theorem image_const_mul_Ioi_zero (ha : 0 < a) :
    (a * ·) '' Ioi 0 = Ioi 0 := by
  rw [image_mul_left_Ioi ha, mul_zero]
Image of $(0, \infty)$ under scaling by a positive element is $(0, \infty)$
Informal description
For any positive element $a$ in a commutative group with zero $G₀$, the image of the open right-infinite interval $(0, \infty)$ under the function $x \mapsto a \cdot x$ is again $(0, \infty)$. That is: $$\{a \cdot x \mid x > 0\} = \{y \mid y > 0\}$$
Set.inv_Ioo_0_left theorem
(ha : 0 < a) : (Ioo 0 a)⁻¹ = Ioi a⁻¹
Full source 
/-- The (pre)image under `inv` of `Ioo 0 a` is `Ioi a⁻¹`. -/
theorem inv_Ioo_0_left (ha : 0 < a) : (Ioo 0 a)⁻¹ = Ioi a⁻¹ := by
  ext x
  exact ⟨fun h ↦ inv_lt_of_inv_lt₀ (inv_pos.1 h.1) h.2,
         fun h ↦ ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_lt_of_inv_lt₀ ha h⟩⟩
Reciprocal Image of $(0, a)$ is $(a^{-1}, \infty)$
Informal description
For any positive real number $a > 0$, the image of the open interval $(0, a)$ under the reciprocal function $x \mapsto x^{-1}$ is the open interval $(a^{-1}, \infty)$.
Set.inv_Ioi₀ theorem
(ha : 0 < a) : (Ioi a)⁻¹ = Ioo 0 a⁻¹
Full source 
theorem inv_Ioi₀ (ha : 0 < a) : (Ioi a)⁻¹ = Ioo 0 a⁻¹ := by
  rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]
Reciprocal Image of $(a, \infty)$ is $(0, a^{-1})$
Informal description
For any positive real number $a > 0$, the image of the open interval $(a, \infty)$ under the reciprocal function $x \mapsto x^{-1}$ is the open interval $(0, a^{-1})$.
Set.preimage_const_mul_Iic theorem
(a : G₀) (h : 0 < c) : (c * ·) ⁻¹' Iic a = Iic (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Iic (a : G₀) (h : 0 < c) : (c * ·) ⁻¹' Iic a = Iic (a / c) :=
  ext fun _x => (le_div_iff₀' h).symm
Preimage of $(-\infty, a]$ under scaling by $c > 0$ is $(-\infty, a/c]$
Informal description
Let $G₀$ be a commutative group with zero, and let $a, c \in G₀$ with $c > 0$. The preimage of the closed interval $(-\infty, a]$ under the function $x \mapsto c \cdot x$ is the closed interval $(-\infty, a/c]$.
Set.preimage_const_mul_Ici theorem
(a : G₀) (h : 0 < c) : (c * ·) ⁻¹' Ici a = Ici (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Ici (a : G₀) (h : 0 < c) : (c * ·) ⁻¹' Ici a = Ici (a / c) :=
  ext fun _x => (div_le_iff₀' h).symm
Preimage of $[a, \infty)$ under Scaling by Positive $c$ in a Commutative Group with Zero
Informal description
For any elements $a, c$ in a commutative group with zero $G₀$, if $c > 0$, then the preimage of the closed interval $[a, \infty)$ under the function $x \mapsto c \cdot x$ is equal to the closed interval $[a/c, \infty)$.
Set.preimage_const_mul_Icc theorem
(a b : G₀) {c : G₀} (h : 0 < c) : (c * ·) ⁻¹' Icc a b = Icc (a / c) (b / c)
Full source 
@[simp]
theorem preimage_const_mul_Icc (a b : G₀) {c : G₀} (h : 0 < c) :
    (c * ·) ⁻¹' Icc a b = Icc (a / c) (b / c) := by simp [← Ici_inter_Iic, h]
Preimage of $[a, b]$ under scaling by $c > 0$ is $[a/c, b/c]$
Informal description
For any elements $a, b, c$ in a commutative group with zero $G₀$, if $c > 0$, then the preimage of the closed interval $[a, b]$ under the function $x \mapsto c \cdot x$ is equal to the closed interval $[a/c, b/c]$. In other words: $$ \{x \in G₀ \mid c \cdot x \in [a, b]\} = [a/c, b/c] $$
Set.preimage_const_mul_Iio theorem
(a : G₀) (h : 0 < c) : (c * ·) ⁻¹' Iio a = Iio (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Iio (a : G₀) (h : 0 < c) : (c * ·) ⁻¹' Iio a = Iio (a / c) :=
  ext fun _x => (lt_div_iff₀' h).symm
Preimage of Left-Infinite Open Interval under Scaling by Positive Constant
Informal description
Let $G₀$ be a commutative group with zero, and let $a, c \in G₀$ with $c > 0$. The preimage of the open left-infinite interval $(-\infty, a)$ under the function $x \mapsto c \cdot x$ is equal to the open left-infinite interval $(-\infty, a/c)$. In other words: $$\{x \in G₀ \mid c \cdot x < a\} = \{x \in G₀ \mid x < a/c\}$$
Set.preimage_const_mul_Ioi theorem
(a : G₀) (h : 0 < c) : (c * ·) ⁻¹' Ioi a = Ioi (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Ioi (a : G₀) (h : 0 < c) : (c * ·) ⁻¹' Ioi a = Ioi (a / c) :=
  ext fun _x => (div_lt_iff₀' h).symm
Preimage of right-infinite interval under positive scaling in a commutative group with zero
Informal description
Let $G₀$ be a commutative group with zero. For any elements $a, c \in G₀$ with $c > 0$, the preimage of the open right-infinite interval $(a, \infty)$ under the function $x \mapsto c \cdot x$ is equal to the open right-infinite interval $(a/c, \infty)$. In other words: $$(c \cdot )^{-1}((a, \infty)) = (a/c, \infty)$$
Set.preimage_const_mul_Ioo theorem
(a b : G₀) (h : 0 < c) : (c * ·) ⁻¹' Ioo a b = Ioo (a / c) (b / c)
Full source 
@[simp]
theorem preimage_const_mul_Ioo (a b : G₀) (h : 0 < c) :
    (c * ·) ⁻¹' Ioo a b = Ioo (a / c) (b / c) := by simp [← Ioi_inter_Iio, h]
Preimage of Open Interval under Positive Scaling in a Commutative Group with Zero
Informal description
Let $G₀$ be a commutative group with zero, and let $a, b, c \in G₀$ with $c > 0$. The preimage of the open interval $(a, b)$ under the function $x \mapsto c \cdot x$ is equal to the open interval $(a/c, b/c)$. In other words: $$\{x \in G₀ \mid a < c \cdot x < b\} = \{x \in G₀ \mid a/c < x < b/c\}$$
Set.preimage_const_mul_Ioc theorem
(a b : G₀) (h : 0 < c) : (c * ·) ⁻¹' Ioc a b = Ioc (a / c) (b / c)
Full source 
@[simp]
theorem preimage_const_mul_Ioc (a b : G₀) (h : 0 < c) :
    (c * ·) ⁻¹' Ioc a b = Ioc (a / c) (b / c) := by simp [← Ioi_inter_Iic, h]
Preimage of $(a, b]$ under scaling by $c > 0$ is $(a/c, b/c]$
Informal description
Let $G₀$ be a commutative group with zero, and let $a, b, c \in G₀$ with $c > 0$. The preimage of the half-open interval $(a, b]$ under the function $x \mapsto c \cdot x$ is the half-open interval $(a/c, b/c]$.
Set.preimage_const_mul_Ico theorem
(a b : G₀) (h : 0 < c) : (c * ·) ⁻¹' Ico a b = Ico (a / c) (b / c)
Full source 
@[simp]
theorem preimage_const_mul_Ico (a b : G₀) (h : 0 < c) :
    (c * ·) ⁻¹' Ico a b = Ico (a / c) (b / c) := by simp [← Ici_inter_Iio, h]
Preimage of Half-Open Interval under Scaling by Positive Constant: $(c \cdot)^{-1}[a, b) = [a/c, b/c)$
Informal description
For any elements $a, b, c$ in a commutative group with zero $G₀$, if $c > 0$, then the preimage of the half-open interval $[a, b)$ under the function $x \mapsto c \cdot x$ is equal to the half-open interval $[a/c, b/c)$.
Set.image_affine_Icc' theorem
(h : 0 < a) (b c d : K) : (a * · + b) '' Icc c d = Icc (a * c + b) (a * d + b)
Full source 
@[simp]
theorem image_affine_Icc' (h : 0 < a) (b c d : K) :
    (a * · + b) '' Icc c d = Icc (a * c + b) (a * d + b) := by
  suffices (· + b) '' ((a * ·) '' Icc c d) = Icc (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
  rw [image_mul_left_Icc' h, image_add_const_Icc]
Image of Closed Interval under Affine Transformation with Positive Slope
Informal description
Let $K$ be a field and let $a, b, c, d \in K$ with $0 < a$. The image of the closed interval $[c, d]$ under the affine transformation $x \mapsto a \cdot x + b$ is the closed interval $[a \cdot c + b, a \cdot d + b]$. In other words: $$\{a \cdot x + b \mid x \in [c, d]\} = [a \cdot c + b, a \cdot d + b]$$
Set.image_affine_Ico theorem
(h : 0 < a) (b c d : K) : (a * · + b) '' Ico c d = Ico (a * c + b) (a * d + b)
Full source 
@[simp]
theorem image_affine_Ico (h : 0 < a) (b c d : K) :
    (a * · + b) '' Ico c d = Ico (a * c + b) (a * d + b) := by
  suffices (· + b) '' ((a * ·) '' Ico c d) = Ico (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
  rw [image_mul_left_Ico h, image_add_const_Ico]
Image of $[c, d)$ under affine transformation $x \mapsto a x + b$ is $[a c + b, a d + b)$
Informal description
Let $K$ be a semifield and let $a, b, c, d \in K$ with $a > 0$. The image of the left-closed right-open interval $[c, d)$ under the affine transformation $x \mapsto a \cdot x + b$ is the left-closed right-open interval $[a \cdot c + b, a \cdot d + b)$.
Set.image_affine_Ioc theorem
(h : 0 < a) (b c d : K) : (a * · + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
Full source 
@[simp]
theorem image_affine_Ioc (h : 0 < a) (b c d : K) :
    (a * · + b) '' Ioc c d = Ioc (a * c + b) (a * d + b) := by
  suffices (· + b) '' ((a * ·) '' Ioc c d) = Ioc (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
  rw [image_mul_left_Ioc h, image_add_const_Ioc]
Image of $(c, d]$ under Affine Transformation $x \mapsto a x + b$ for $a > 0$
Informal description
Let $K$ be a semifield and let $a > 0$ be a positive element. For any elements $b, c, d \in K$, the image of the left-open right-closed interval $(c, d]$ under the affine transformation $x \mapsto a \cdot x + b$ is the left-open right-closed interval $(a \cdot c + b, a \cdot d + b]$.
Set.image_affine_Ioo theorem
(h : 0 < a) (b c d : K) : (a * · + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
Full source 
@[simp]
theorem image_affine_Ioo (h : 0 < a) (b c d : K) :
    (a * · + b) '' Ioo c d = Ioo (a * c + b) (a * d + b) := by
  suffices (· + b) '' ((a * ·) '' Ioo c d) = Ioo (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
  rw [image_mul_left_Ioo h, image_add_const_Ioo]
Image of Open Interval under Affine Transformation with Positive Slope
Informal description
Let $K$ be a linearly ordered field. For any positive element $a \in K$ (i.e., $0 < a$) and any elements $b, c, d \in K$, the image of the open interval $(c, d)$ under the affine transformation $x \mapsto a \cdot x + b$ is equal to the open interval $(a \cdot c + b, a \cdot d + b)$.
Set.preimage_mul_const_Iio_of_neg theorem
(a : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Iio a = Ioi (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Iio_of_neg (a : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Iio a = Ioi (a / c) :=
  ext fun _x => (div_lt_iff_of_neg h).symm
Preimage of $(-\infty, a)$ under $x \mapsto x \cdot c$ for negative $c$ is $(a/c, \infty)$
Informal description
For any elements $a$ and $c$ in a linearly ordered field $\alpha$, if $c < 0$, then the preimage of the open interval $(-\infty, a)$ under the function $x \mapsto x \cdot c$ is equal to the open interval $(a/c, \infty)$.
Set.preimage_mul_const_Ioi_of_neg theorem
(a : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Ioi a = Iio (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Ioi_of_neg (a : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Ioi a = Iio (a / c) :=
  ext fun _x => (lt_div_iff_of_neg h).symm
Preimage of Right-Infinite Interval under Negative Scaling
Informal description
Let $α$ be a type with a linear order and multiplication. For any elements $a, c \in α$ with $c < 0$, the preimage of the open right-infinite interval $(a, \infty)$ under the function $x \mapsto x \cdot c$ is equal to the open left-infinite interval $(-\infty, a/c)$. In other words: $$\{x \in α \mid x \cdot c > a\} = \{x \in α \mid x < a/c\}$$
Set.preimage_mul_const_Iic_of_neg theorem
(a : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Iic a = Ici (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Iic_of_neg (a : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Iic a = Ici (a / c) :=
  ext fun _x => (div_le_iff_of_neg h).symm
Preimage of $(-\infty, a]$ under negative scaling equals $[a/c, \infty)$
Informal description
Let $\alpha$ be a type with a linear order and multiplication. For any $a, c \in \alpha$ with $c < 0$, the preimage of the closed interval $(-\infty, a]$ under the function $x \mapsto x \cdot c$ is equal to the closed interval $[a/c, \infty)$. In other words: $$ \{x \in \alpha \mid x \cdot c \leq a\} = \{x \in \alpha \mid x \geq a/c\} $$
Set.preimage_mul_const_Ici_of_neg theorem
(a : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Ici a = Iic (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Ici_of_neg (a : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Ici a = Iic (a / c) :=
  ext fun _x => (le_div_iff_of_neg h).symm
Preimage of $[a,\infty)$ under negative scaling equals $(-\infty, a/c]$
Informal description
Let $α$ be an ordered type and let $c < 0$ be a negative element in $α$. For any $a \in α$, the preimage of the closed upper interval $[a, \infty)$ under the function $x \mapsto x \cdot c$ equals the closed lower interval $(-\infty, a/c]$.
Set.preimage_mul_const_Ioo_of_neg theorem
(a b : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Ioo_of_neg (a b : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c) := by simp [← Ioi_inter_Iio, h, inter_comm]
Preimage of $(a, b)$ under negative scaling is $(b/c, a/c)$
Informal description
Let $\alpha$ be a linearly ordered field. For any elements $a, b \in \alpha$ and any negative element $c < 0$, the preimage of the open interval $(a, b)$ under the function $x \mapsto x \cdot c$ is equal to the open interval $(b/c, a/c)$. In other words: $$\{x \in \alpha \mid a < x \cdot c < b\} = (b/c, a/c)$$
Set.preimage_mul_const_Ioc_of_neg theorem
(a b : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Ioc_of_neg (a b : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Ioc a b = Ico (b / c) (a / c) := by
  simp [← Ioi_inter_Iic, ← Ici_inter_Iio, h, inter_comm]
Preimage of $(a, b]$ under negative scaling is $[b/c, a/c)$
Informal description
Let $\alpha$ be a linearly ordered field. For any elements $a, b \in \alpha$ and any negative element $c < 0$, the preimage of the half-open interval $(a, b]$ under the function $x \mapsto x \cdot c$ is equal to the half-open interval $[b/c, a/c)$. In other words: $$\{x \in \alpha \mid a < x \cdot c \leq b\} = [b/c, a/c)$$
Set.preimage_mul_const_Ico_of_neg theorem
(a b : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Ico_of_neg (a b : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c) := by
  simp [← Ici_inter_Iio, ← Ioi_inter_Iic, h, inter_comm]
Preimage of $[a,b)$ under negative scaling equals $(b/c, a/c]$
Informal description
Let $α$ be a linearly ordered field, and let $a, b, c \in α$ with $c < 0$. The preimage of the half-open interval $[a, b)$ under the function $x \mapsto x \cdot c$ is equal to the half-open interval $(b/c, a/c]$.
Set.preimage_mul_const_Icc_of_neg theorem
(a b : α) {c : α} (h : c < 0) : (fun x => x * c) ⁻¹' Icc a b = Icc (b / c) (a / c)
Full source 
@[simp]
theorem preimage_mul_const_Icc_of_neg (a b : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Icc a b = Icc (b / c) (a / c) := by simp [← Ici_inter_Iic, h, inter_comm]
Preimage of $[a,b]$ under negative scaling equals $[b/c, a/c]$
Informal description
Let $\alpha$ be a linearly ordered type with multiplication and division. For any $a, b \in \alpha$ and any negative $c \in \alpha$ (i.e., $c < 0$), the preimage of the closed interval $[a, b]$ under the function $x \mapsto x \cdot c$ is equal to the closed interval $[b/c, a/c]$. In other words: $$ \{x \in \alpha \mid a \leq x \cdot c \leq b\} = \{x \in \alpha \mid b/c \leq x \leq a/c\} $$
Set.preimage_const_mul_Iio_of_neg theorem
(a : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Iio a = Ioi (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Iio_of_neg (a : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Iio a = Ioi (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Iio_of_neg a h
Preimage of $(-\infty, a)$ under scaling by negative $c$ is $(a/c, \infty)$
Informal description
For any elements $a$ and $c$ in a linearly ordered field $\alpha$, if $c < 0$, then the preimage of the open interval $(-\infty, a)$ under the function $x \mapsto c \cdot x$ is equal to the open interval $(a/c, \infty)$.
Set.preimage_const_mul_Ioi_of_neg theorem
(a : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Ioi a = Iio (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Ioi_of_neg (a : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ioi a = Iio (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h
Preimage of Right-Infinite Interval under Negative Left Scaling
Informal description
Let $α$ be a linearly ordered type with multiplication. For any elements $a, c \in α$ with $c < 0$, the preimage of the open right-infinite interval $(a, \infty)$ under the function $x \mapsto c \cdot x$ is equal to the open left-infinite interval $(-\infty, a/c)$. In other words: $$\{x \in α \mid c \cdot x > a\} = \{x \in α \mid x < a/c\}$$
Set.preimage_const_mul_Iic_of_neg theorem
(a : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Iic a = Ici (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Iic_of_neg (a : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Iic a = Ici (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Iic_of_neg a h
Preimage of $(-\infty, a]$ under negative left-multiplication equals $[a/c, \infty)$
Informal description
Let $\alpha$ be a linearly ordered type with multiplication. For any elements $a, c \in \alpha$ with $c < 0$, the preimage of the closed interval $(-\infty, a]$ under the function $x \mapsto c \cdot x$ is equal to the closed interval $[a/c, \infty)$. In other words: $$ \{x \in \alpha \mid c \cdot x \leq a\} = \{x \in \alpha \mid x \geq a/c\} $$
Set.preimage_const_mul_Ici_of_neg theorem
(a : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Ici a = Iic (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Ici_of_neg (a : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ici a = Iic (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Ici_of_neg a h
Preimage of $[a,\infty)$ under negative left-multiplication equals $(-\infty, a/c]$
Informal description
Let $\alpha$ be a linearly ordered type with multiplication. For any elements $a, c \in \alpha$ with $c < 0$, the preimage of the closed interval $[a, \infty)$ under the function $x \mapsto c \cdot x$ is equal to the closed interval $(-\infty, a/c]$. In other words: $$ \{x \in \alpha \mid c \cdot x \geq a\} = \{x \in \alpha \mid x \leq a/c\} $$
Set.preimage_const_mul_Ioo_of_neg theorem
(a b : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Ioo a b = Ioo (b / c) (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Ioo_of_neg (a b : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ioo a b = Ioo (b / c) (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Ioo_of_neg a b h
Preimage of $(a, b)$ under negative left-multiplication is $(b/c, a/c)$
Informal description
Let $\alpha$ be a linearly ordered field. For any elements $a, b \in \alpha$ and any negative element $c < 0$, the preimage of the open interval $(a, b)$ under the function $x \mapsto c \cdot x$ is equal to the open interval $(b/c, a/c)$. In other words: $$\{x \in \alpha \mid a < c \cdot x < b\} = (b/c, a/c)$$
Set.preimage_const_mul_Ioc_of_neg theorem
(a b : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Ioc a b = Ico (b / c) (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Ioc_of_neg (a b : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ioc a b = Ico (b / c) (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Ioc_of_neg a b h
Preimage of $(a, b]$ under negative left-multiplication is $[b/c, a/c)$
Informal description
Let $\alpha$ be a linearly ordered field. For any elements $a, b \in \alpha$ and any negative element $c < 0$, the preimage of the half-open interval $(a, b]$ under the function $x \mapsto c \cdot x$ is equal to the half-closed interval $[b/c, a/c)$. In other words: $$\{x \in \alpha \mid a < c \cdot x \leq b\} = [b/c, a/c)$$
Set.preimage_const_mul_Ico_of_neg theorem
(a b : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Ico a b = Ioc (b / c) (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Ico_of_neg (a b : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ico a b = Ioc (b / c) (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Ico_of_neg a b h
Preimage of $[a,b)$ under negative left-multiplication equals $(b/c, a/c]$
Informal description
Let $\alpha$ be a linearly ordered field. For any elements $a, b \in \alpha$ and any negative element $c < 0$, the preimage of the half-open interval $[a, b)$ under the function $x \mapsto c \cdot x$ is equal to the half-open interval $(b/c, a/c]$. In other words: $$\{x \in \alpha \mid a \leq c \cdot x < b\} = (b/c, a/c]$$
Set.preimage_const_mul_Icc_of_neg theorem
(a b : α) {c : α} (h : c < 0) : (c * ·) ⁻¹' Icc a b = Icc (b / c) (a / c)
Full source 
@[simp]
theorem preimage_const_mul_Icc_of_neg (a b : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Icc a b = Icc (b / c) (a / c) := by
  simpa only [mul_comm] using preimage_mul_const_Icc_of_neg a b h
Preimage of $[a,b]$ under negative left-multiplication equals $[b/c, a/c]$
Informal description
Let $\alpha$ be a linearly ordered field. For any elements $a, b \in \alpha$ and any negative element $c \in \alpha$ (i.e., $c < 0$), the preimage of the closed interval $[a, b]$ under the function $x \mapsto c \cdot x$ is equal to the closed interval $[b/c, a/c]$. In other words: $$\{x \in \alpha \mid a \leq c \cdot x \leq b\} = [b/c, a/c]$$
Set.preimage_mul_const_uIcc theorem
(ha : a ≠ 0) (b c : α) : (· * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
Full source 
@[simp]
theorem preimage_mul_const_uIcc (ha : a ≠ 0) (b c : α) :
    (· * a) ⁻¹' [[b, c]] = [[b / a, c / a]] :=
  (lt_or_gt_of_ne ha).elim
    (fun h => by
      simp [← Icc_min_max, h, h.le, min_div_div_right_of_nonpos, max_div_div_right_of_nonpos])
    fun ha : 0 < a => by simp [← Icc_min_max, ha, ha.le, min_div_div_right, max_div_div_right]
Preimage of Closed Interval under Right Multiplication by Nonzero Scalar
Informal description
Let $\alpha$ be a type with multiplication and division, and let $a, b, c \in \alpha$ with $a \neq 0$. The preimage of the closed interval $[b, c]$ under the function $x \mapsto x \cdot a$ is equal to the closed interval $\left[\frac{b}{a}, \frac{c}{a}\right]$. In mathematical notation: $$(x \mapsto x \cdot a)^{-1}\big([b, c]\big) = \left[\frac{b}{a}, \frac{c}{a}\right]$$
Set.preimage_const_mul_uIcc theorem
(ha : a ≠ 0) (b c : α) : (a * ·) ⁻¹' [[b, c]] = [[b / a, c / a]]
Full source 
@[simp]
theorem preimage_const_mul_uIcc (ha : a ≠ 0) (b c : α) :
    (a * ·) ⁻¹' [[b, c]] = [[b / a, c / a]] := by
  simp only [← preimage_mul_const_uIcc ha, mul_comm]
Preimage of Closed Interval under Left Multiplication by Nonzero Scalar
Informal description
Let $\alpha$ be a type with multiplication and division, and let $a, b, c \in \alpha$ with $a \neq 0$. The preimage of the closed interval $[b, c]$ under the function $x \mapsto a \cdot x$ is equal to the closed interval $\left[\frac{b}{a}, \frac{c}{a}\right]$. In mathematical notation: $$(x \mapsto a \cdot x)^{-1}\big([b, c]\big) = \left[\frac{b}{a}, \frac{c}{a}\right]$$
Set.preimage_div_const_uIcc theorem
(ha : a ≠ 0) (b c : α) : (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]
Full source 
@[simp]
theorem preimage_div_const_uIcc (ha : a ≠ 0) (b c : α) :
    (fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]] := by
  simp only [div_eq_mul_inv, preimage_mul_const_uIcc (inv_ne_zero ha), inv_inv]
Preimage of Closed Interval under Division by Nonzero Scalar
Informal description
Let $\alpha$ be a type with multiplication and division, and let $a, b, c \in \alpha$ with $a \neq 0$. The preimage of the closed interval $[b, c]$ under the function $x \mapsto x / a$ is equal to the closed interval $[b \cdot a, c \cdot a]$. In mathematical notation: $$(x \mapsto x / a)^{-1}\big([b, c]\big) = [b \cdot a, c \cdot a]$$
Set.preimage_const_mul_Ioi_or_Iio theorem
(hb : a ≠ 0) {U V : Set α} (hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}) (hV : V = (a * ·) ⁻¹' U) : V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
Full source 
lemma preimage_const_mul_Ioi_or_Iio (hb : a ≠ 0) {U V : Set α}
    (hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}) (hV : V = (a * ·) ⁻¹' U) :
    V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a} := by
  obtain ⟨aU, (haU | haU)⟩ := hU <;>
  simp only [hV, haU, mem_setOf_eq] <;>
  use a⁻¹ * aU <;>
  rcases lt_or_gt_of_ne hb with (hb | hb)
  · right; rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]
  · left; rw [Set.preimage_const_mul_Ioi _ hb, div_eq_inv_mul]
  · left; rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]
  · right; rw [Set.preimage_const_mul_Iio _ hb, div_eq_inv_mul]
Preimage of One-Sided Infinite Interval under Scaling by Nonzero Constant Preserves Interval Type
Informal description
Let $\alpha$ be a type with multiplication and let $a \in \alpha$ be nonzero. For any set $U$ that is either an open right-infinite interval $(b, \infty)$ or an open left-infinite interval $(-\infty, b)$ for some $b \in \alpha$, the preimage $V$ of $U$ under the function $x \mapsto a \cdot x$ is also of the same form (i.e., either $(b/a, \infty)$ or $(-\infty, b/a)$ if $a > 0$, or $(-\infty, b/a)$ or $(b/a, \infty)$ if $a < 0$).
Set.image_mul_const_uIcc theorem
(a b c : α) : (· * a) '' [[b, c]] = [[b * a, c * a]]
Full source 
@[simp]
theorem image_mul_const_uIcc (a b c : α) : (· * a) '' [[b, c]] = [[b * a, c * a]] :=
  if ha : a = 0 then by simp [ha]
  else calc
    (fun x => x * a) '' [[b, c]] = (· * a⁻¹) ⁻¹' [[b, c]] :=
      (Units.mk0 a ha).mulRight.image_eq_preimage _
    _ = (fun x => x / a) ⁻¹' [[b, c]] := by simp only [div_eq_mul_inv]
    _ = [[b * a, c * a]] := preimage_div_const_uIcc ha _ _
Image of Closed Interval under Right Multiplication by Scalar
Informal description
For any elements $a, b, c$ in a type $\alpha$ with multiplication, the image of the closed interval $[b, c]$ under the function $x \mapsto x \cdot a$ is equal to the closed interval $[b \cdot a, c \cdot a]$. In mathematical notation: $$(x \mapsto x \cdot a)\big([b, c]\big) = [b \cdot a, c \cdot a]$$
Set.image_const_mul_uIcc theorem
(a b c : α) : (a * ·) '' [[b, c]] = [[a * b, a * c]]
Full source 
@[simp]
theorem image_const_mul_uIcc (a b c : α) : (a * ·) '' [[b, c]] = [[a * b, a * c]] := by
  simpa only [mul_comm] using image_mul_const_uIcc a b c
Image of Closed Interval under Left Multiplication by Scalar
Informal description
For any elements $a, b, c$ in a type $\alpha$ with multiplication, the image of the closed interval $[b, c]$ under the function $x \mapsto a \cdot x$ is equal to the closed interval $[a \cdot b, a \cdot c]$. In mathematical notation: $$(x \mapsto a \cdot x)\big([b, c]\big) = [a \cdot b, a \cdot c]$$
Set.image_div_const_uIcc theorem
(a b c : α) : (fun x => x / a) '' [[b, c]] = [[b / a, c / a]]
Full source 
@[simp]
theorem image_div_const_uIcc (a b c : α) : (fun x => x / a) '' [[b, c]] = [[b / a, c / a]] := by
  simp only [div_eq_mul_inv, image_mul_const_uIcc]
Image of Closed Interval under Division by Scalar
Informal description
For any elements $a, b, c$ in a type $\alpha$ with division, the image of the closed interval $[b, c]$ under the function $x \mapsto x / a$ is equal to the closed interval $[b / a, c / a]$. In mathematical notation: $$(x \mapsto x / a)\big([b, c]\big) = [b / a, c / a]$$
Set.inv_Ioo_0_right theorem
{a : α} (ha : a < 0) : (Ioo a 0)⁻¹ = Iio a⁻¹
Full source 
/-- The (pre)image under `inv` of `Ioo a 0` is `Iio a⁻¹`. -/
theorem inv_Ioo_0_right {a : α} (ha : a < 0) : (Ioo a 0)⁻¹ = Iio a⁻¹ := by
  ext x
  refine ⟨fun h ↦ (lt_inv_of_neg (inv_neg''.1 h.2) ha).2 h.1, fun h ↦ ?_⟩
  have h' := (h.trans (inv_neg''.2 ha))
  exact ⟨(lt_inv_of_neg ha h').2 h, inv_neg''.2 h'⟩
Inversion maps $(a, 0)$ to $(-\infty, a^{-1})$ for $a < 0$
Informal description
For any negative real number $a < 0$, the image of the open interval $(a, 0)$ under the inversion function $x \mapsto x^{-1}$ is the open left-infinite interval $(-\infty, a^{-1})$.
Set.inv_Iio₀ theorem
{a : α} (ha : a < 0) : (Iio a)⁻¹ = Ioo a⁻¹ 0
Full source 
theorem inv_Iio₀ {a : α} (ha : a < 0) : (Iio a)⁻¹ = Ioo a⁻¹ 0 := by
  rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]
Inversion maps $(-\infty, a)$ to $(a^{-1}, 0)$ for $a < 0$
Informal description
For any negative real number $a < 0$, the image of the open left-infinite interval $(-\infty, a)$ under the inversion function $x \mapsto x^{-1}$ is the open interval $(a^{-1}, 0)$.