Mathlib.Algebra.Order.Interval.Set.Monoid

Set.Ici_add_bij theorem

: BijOn (· + d) (Ici a) (Ici (a + d))

Full source

theorem Ici_add_bij : BijOn (· + d) (Ici a) (Ici (a + d)) := by
  refine
    ⟨fun x h => add_le_add_right (mem_Ici.mp h) _, (add_left_injective d).injOn, fun _ h => ?_⟩
  obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)
  rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h
  exact ⟨a + c, h, by rw [add_right_comm]⟩

Bijectivity of Right Translation on $[a, \infty)$: $x \mapsto x + d$

Informal description

For any element $d$ in an ordered cancellative additive monoid $\alpha$, the function $x \mapsto x + d$ is a bijection from the interval $[a, \infty)$ to the interval $[a + d, \infty)$.

Set.Ioi_add_bij theorem

: BijOn (· + d) (Ioi a) (Ioi (a + d))

Full source

theorem Ioi_add_bij : BijOn (· + d) (Ioi a) (Ioi (a + d)) := by
  refine
    ⟨fun x h => add_lt_add_right (mem_Ioi.mp h) _, fun _ _ _ _ h => add_right_cancel h, fun _ h =>
      ?_⟩
  obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le
  rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h
  exact ⟨a + c, h, by rw [add_right_comm]⟩

Bijectivity of Right Translation on Left-Open Right-Infinite Intervals in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, d \in \alpha$. The function $x \mapsto x + d$ is a bijection from the left-open right-infinite interval $(a, \infty)$ to the interval $(a + d, \infty)$.

Set.Icc_add_bij theorem

: BijOn (· + d) (Icc a b) (Icc (a + d) (b + d))

Full source

theorem Icc_add_bij : BijOn (· + d) (Icc a b) (Icc (a + d) (b + d)) := by
  rw [← Ici_inter_Iic, ← Ici_inter_Iic]
  exact
    (Ici_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx =>
      le_of_add_le_add_right hx.2

Bijectivity of Right Translation on Closed Intervals: $x \mapsto x + d$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, d \in \alpha$. The function $x \mapsto x + d$ is a bijection from the closed interval $[a, b]$ to the closed interval $[a + d, b + d]$.

Set.Ioo_add_bij theorem

: BijOn (· + d) (Ioo a b) (Ioo (a + d) (b + d))

Full source

theorem Ioo_add_bij : BijOn (· + d) (Ioo a b) (Ioo (a + d) (b + d)) := by
  rw [← Ioi_inter_Iio, ← Ioi_inter_Iio]
  exact
    (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx =>
      lt_of_add_lt_add_right hx.2

Bijectivity of Right Translation on Open Intervals in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, d \in \alpha$. The function $x \mapsto x + d$ is a bijection from the open interval $(a, b)$ to the open interval $(a + d, b + d)$.

Set.Ioc_add_bij theorem

: BijOn (· + d) (Ioc a b) (Ioc (a + d) (b + d))

Full source

theorem Ioc_add_bij : BijOn (· + d) (Ioc a b) (Ioc (a + d) (b + d)) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic]
  exact
    (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx =>
      le_of_add_le_add_right hx.2

Bijectivity of Right Translation on Left-Open Right-Closed Intervals in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, d \in \alpha$. The function $x \mapsto x + d$ is a bijection from the left-open right-closed interval $(a, b]$ to the interval $(a + d, b + d]$.

Set.Ico_add_bij theorem

: BijOn (· + d) (Ico a b) (Ico (a + d) (b + d))

Full source

theorem Ico_add_bij : BijOn (· + d) (Ico a b) (Ico (a + d) (b + d)) := by
  rw [← Ici_inter_Iio, ← Ici_inter_Iio]
  exact
    (Ici_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx =>
      lt_of_add_lt_add_right hx.2

Bijectivity of Right Translation on $[a, b)$: $x \mapsto x + d$

Informal description

For any elements $a, b, d$ in an ordered cancellative additive monoid $\alpha$, the function $x \mapsto x + d$ is a bijection from the interval $[a, b)$ to the interval $[a + d, b + d)$.

Set.image_add_const_Ici theorem

: (fun x => x + a) '' Ici b = Ici (b + a)

Full source

@[simp]
theorem image_add_const_Ici : (fun x => x + a) '' Ici b = Ici (b + a) :=
  (Ici_add_bij _ _).image_eq

Image of $[b, \infty)$ under Right Translation by $a$: $(x \mapsto x + a)([b, \infty)) = [b + a, \infty)$

Informal description

For any elements $a$ and $b$ in an ordered cancellative additive monoid $\alpha$, the image of the interval $[b, \infty)$ under the function $x \mapsto x + a$ is equal to the interval $[b + a, \infty)$. That is, $(x \mapsto x + a)([b, \infty)) = [b + a, \infty)$.

Set.image_add_const_Ioi theorem

: (fun x => x + a) '' Ioi b = Ioi (b + a)

Full source

@[simp]
theorem image_add_const_Ioi : (fun x => x + a) '' Ioi b = Ioi (b + a) :=
  (Ioi_add_bij _ _).image_eq

Image of Right Translation on $(b, \infty)$ is $(b + a, \infty)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b \in \alpha$. The image of the left-open right-infinite interval $(b, \infty)$ under the function $x \mapsto x + a$ is the interval $(b + a, \infty)$.

Set.image_add_const_Icc theorem

: (fun x => x + a) '' Icc b c = Icc (b + a) (c + a)

Full source

@[simp]
theorem image_add_const_Icc : (fun x => x + a) '' Icc b c = Icc (b + a) (c + a) :=
  (Icc_add_bij _ _ _).image_eq

Image of Closed Interval under Right Translation by $a$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, c \in \alpha$. The image of the closed interval $[b, c]$ under the function $x \mapsto x + a$ is the closed interval $[b + a, c + a]$. That is, $(x \mapsto x + a)([b, c]) = [b + a, c + a]$.

Set.image_add_const_Ico theorem

: (fun x => x + a) '' Ico b c = Ico (b + a) (c + a)

Full source

@[simp]
theorem image_add_const_Ico : (fun x => x + a) '' Ico b c = Ico (b + a) (c + a) :=
  (Ico_add_bij _ _ _).image_eq

Image of $[b, c)$ under right translation by $a$ is $[b + a, c + a)$

Informal description

For any elements $a, b, c$ in an ordered cancellative additive monoid $\alpha$, the image of the interval $[b, c)$ under the function $x \mapsto x + a$ is the interval $[b + a, c + a)$.

Set.image_add_const_Ioc theorem

: (fun x => x + a) '' Ioc b c = Ioc (b + a) (c + a)

Full source

@[simp]
theorem image_add_const_Ioc : (fun x => x + a) '' Ioc b c = Ioc (b + a) (c + a) :=
  (Ioc_add_bij _ _ _).image_eq

Image of Right Translation on $(b, c]$ is $(b + a, c + a]$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, c \in \alpha$. The image of the left-open right-closed interval $(b, c]$ under the function $x \mapsto x + a$ is the left-open right-closed interval $(b + a, c + a]$. In other words, $(x + a \mid x \in (b, c]) = (b + a, c + a]$.

Set.image_add_const_Ioo theorem

: (fun x => x + a) '' Ioo b c = Ioo (b + a) (c + a)

Full source

@[simp]
theorem image_add_const_Ioo : (fun x => x + a) '' Ioo b c = Ioo (b + a) (c + a) :=
  (Ioo_add_bij _ _ _).image_eq

Right Translation Preserves Open Intervals in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, c \in \alpha$. The image of the open interval $(b, c)$ under the right translation map $x \mapsto x + a$ is the open interval $(b + a, c + a)$. In other words, $(b, c) + a = (b + a, c + a)$.

Set.image_const_add_Ici theorem

: (fun x => a + x) '' Ici b = Ici (a + b)

Full source

@[simp]
theorem image_const_add_Ici : (fun x => a + x) '' Ici b = Ici (a + b) := by
  simp only [add_comm a, image_add_const_Ici]

Image of $[b, \infty)$ under Left Translation by $a$: $(x \mapsto a + x)([b, \infty)) = [a + b, \infty)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid. For any elements $a, b \in \alpha$, the image of the interval $[b, \infty)$ under the left translation function $x \mapsto a + x$ is equal to the interval $[a + b, \infty)$. That is, $$ \{a + x \mid x \in [b, \infty)\} = [a + b, \infty). $$

Set.image_const_add_Ioi theorem

: (fun x => a + x) '' Ioi b = Ioi (a + b)

Full source

@[simp]
theorem image_const_add_Ioi : (fun x => a + x) '' Ioi b = Ioi (a + b) := by
  simp only [add_comm a, image_add_const_Ioi]

Image of Right Translation on $(b, \infty)$ is $(a + b, \infty)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b \in \alpha$. The image of the left-open right-infinite interval $(b, \infty)$ under the function $x \mapsto a + x$ is the interval $(a + b, \infty)$. That is, $$ \{a + x \mid x > b\} = \{y \mid y > a + b\}. $$

Set.image_const_add_Icc theorem

: (fun x => a + x) '' Icc b c = Icc (a + b) (a + c)

Full source

@[simp]
theorem image_const_add_Icc : (fun x => a + x) '' Icc b c = Icc (a + b) (a + c) := by
  simp only [add_comm a, image_add_const_Icc]

Left Translation Preserves Closed Intervals in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, c \in \alpha$. The image of the closed interval $[b, c]$ under the left translation function $x \mapsto a + x$ is the closed interval $[a + b, a + c]$. That is, $$ \{a + x \mid x \in [b, c]\} = [a + b, a + c]. $$

Set.image_const_add_Ico theorem

: (fun x => a + x) '' Ico b c = Ico (a + b) (a + c)

Full source

@[simp]
theorem image_const_add_Ico : (fun x => a + x) '' Ico b c = Ico (a + b) (a + c) := by
  simp only [add_comm a, image_add_const_Ico]

Image of Left Translation on $[b, c)$ is $[a + b, a + c)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, c \in \alpha$. The image of the left-closed right-open interval $[b, c)$ under the function $x \mapsto a + x$ is the interval $[a + b, a + c)$. That is, $$ \{a + x \mid b \leq x < c\} = \{y \mid a + b \leq y < a + c\}. $$

Set.image_const_add_Ioc theorem

: (fun x => a + x) '' Ioc b c = Ioc (a + b) (a + c)

Full source

@[simp]
theorem image_const_add_Ioc : (fun x => a + x) '' Ioc b c = Ioc (a + b) (a + c) := by
  simp only [add_comm a, image_add_const_Ioc]

Left Translation Preserves Left-Open Right-Closed Intervals in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, c \in \alpha$. The image of the left-open right-closed interval $(b, c]$ under the left translation map $x \mapsto a + x$ is the interval $(a + b, a + c]$. In other words, $$ \{a + x \mid b < x \leq c\} = \{y \mid a + b < y \leq a + c\}. $$

Set.image_const_add_Ioo theorem

: (fun x => a + x) '' Ioo b c = Ioo (a + b) (a + c)

Full source

@[simp]
theorem image_const_add_Ioo : (fun x => a + x) '' Ioo b c = Ioo (a + b) (a + c) := by
  simp only [add_comm a, image_add_const_Ioo]

Left Translation Preserves Open Intervals in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid, and let $a, b, c \in \alpha$. The image of the open interval $(b, c)$ under the left translation map $x \mapsto a + x$ is the open interval $(a + b, a + c)$. In other words, $a + (b, c) = (a + b, a + c)$.