Mathlib.Algebra.Order.Interval.Finset.Basic

Finset.map_add_left_Icc theorem

(a b c : α) : (Icc a b).map (addLeftEmbedding c) = Icc (c + a) (c + b)

Full source

@[simp] lemma map_add_left_Icc (a b c : α) :
    (Icc a b).map (addLeftEmbedding c) = Icc (c + a) (c + b) := by
  rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
  exact Set.image_const_add_Icc _ _ _

Left Translation Preserves Closed Interval Finsets: $c + \text{Icc}(a, b) = \text{Icc}(c + a, c + b)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the closed interval finset $[a, b]$ under the left translation map $x \mapsto c + x$ is equal to the closed interval finset $[c + a, c + b]$. In symbols: $$\text{map}(x \mapsto c + x, \text{Icc}(a, b)) = \text{Icc}(c + a, c + b)$$

Finset.map_add_right_Icc theorem

(a b c : α) : (Icc a b).map (addRightEmbedding c) = Icc (a + c) (b + c)

Full source

@[simp] lemma map_add_right_Icc (a b c : α) :
    (Icc a b).map (addRightEmbedding c) = Icc (a + c) (b + c) := by
  rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
  exact Set.image_add_const_Icc _ _ _

Right Translation Preserves Closed Interval Finsets: $\text{Icc}(a, b) + c = \text{Icc}(a + c, b + c)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the closed interval finset $\text{Icc}(a, b)$ under the right translation map $x \mapsto x + c$ is equal to the closed interval finset $\text{Icc}(a + c, b + c)$. In symbols: $$(\text{Icc}(a, b)).\text{map}(x \mapsto x + c) = \text{Icc}(a + c, b + c)$$

Finset.map_add_left_Ico theorem

(a b c : α) : (Ico a b).map (addLeftEmbedding c) = Ico (c + a) (c + b)

Full source

@[simp] lemma map_add_left_Ico (a b c : α) :
    (Ico a b).map (addLeftEmbedding c) = Ico (c + a) (c + b) := by
  rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
  exact Set.image_const_add_Ico _ _ _

Left translation preserves closed-open intervals: $\text{Ico}(a, b) + c = \text{Ico}(a + c, b + c)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the closed-open interval finset $\text{Ico}(a, b)$ under the left translation map $x \mapsto c + x$ is equal to the closed-open interval finset $\text{Ico}(c + a, c + b)$. In symbols: $$(\text{Ico}(a, b)).\text{map}(x \mapsto c + x) = \text{Ico}(c + a, c + b)$$

Finset.map_add_right_Ico theorem

(a b c : α) : (Ico a b).map (addRightEmbedding c) = Ico (a + c) (b + c)

Full source

@[simp] lemma map_add_right_Ico (a b c : α) :
    (Ico a b).map (addRightEmbedding c) = Ico (a + c) (b + c) := by
  rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
  exact Set.image_add_const_Ico _ _ _

Right translation preserves closed-open intervals: $\text{Ico}(a, b) + c = \text{Ico}(a + c, b + c)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the closed-open interval $[a, b)$ under the right translation map $x \mapsto x + c$ is the closed-open interval $[a + c, b + c)$. In other words, the finset obtained by applying the right translation by $c$ to each element of $\text{Ico}(a, b)$ is equal to the finset $\text{Ico}(a + c, b + c)$.

Finset.map_add_left_Ioc theorem

(a b c : α) : (Ioc a b).map (addLeftEmbedding c) = Ioc (c + a) (c + b)

Full source

@[simp] lemma map_add_left_Ioc (a b c : α) :
    (Ioc a b).map (addLeftEmbedding c) = Ioc (c + a) (c + b) := by
  rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
  exact Set.image_const_add_Ioc _ _ _

Left Translation Preserves Open-Closed Interval: $c + (a, b] = (c + a, c + b]$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the open-closed interval $(a, b]$ under the left translation map $x \mapsto c + x$ is equal to the open-closed interval $(c + a, c + b]$. In other words, $$ \{c + x \mid a < x \leq b\} = \{y \mid c + a < y \leq c + b\}. $$

Finset.map_add_right_Ioc theorem

(a b c : α) : (Ioc a b).map (addRightEmbedding c) = Ioc (a + c) (b + c)

Full source

@[simp] lemma map_add_right_Ioc (a b c : α) :
    (Ioc a b).map (addRightEmbedding c) = Ioc (a + c) (b + c) := by
  rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]
  exact Set.image_add_const_Ioc _ _ _

Right Translation Preserves Open-Closed Interval: $(a, b] + c = (a + c, b + c]$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the finset $(a, b]$ under the right translation map $x \mapsto x + c$ is equal to the finset $(a + c, b + c]$. In other words, $(a, b] + c = (a + c, b + c]$.

Finset.map_add_left_Ioo theorem

(a b c : α) : (Ioo a b).map (addLeftEmbedding c) = Ioo (c + a) (c + b)

Full source

@[simp] lemma map_add_left_Ioo (a b c : α) :
    (Ioo a b).map (addLeftEmbedding c) = Ioo (c + a) (c + b) := by
  rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
  exact Set.image_const_add_Ioo _ _ _

Left Translation Preserves Open Interval Finsets in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the open interval finset $\text{Ioo}(a, b)$ under the left translation map $x \mapsto c + x$ is equal to the open interval finset $\text{Ioo}(c + a, c + b)$. In symbols: $$c + \text{Ioo}(a, b) = \text{Ioo}(c + a, c + b)$$

Finset.map_add_right_Ioo theorem

(a b c : α) : (Ioo a b).map (addRightEmbedding c) = Ioo (a + c) (b + c)

Full source

@[simp] lemma map_add_right_Ioo (a b c : α) :
    (Ioo a b).map (addRightEmbedding c) = Ioo (a + c) (b + c) := by
  rw [← coe_inj, coe_map, coe_Ioo, coe_Ioo]
  exact Set.image_add_const_Ioo _ _ _

Right Translation Preserves Open Interval Finsets in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the open interval finset $\text{Ioo}(a, b)$ under the right translation map $x \mapsto x + c$ is equal to the open interval finset $\text{Ioo}(a + c, b + c)$. In symbols: $$(\text{Ioo}(a, b)) + c = \text{Ioo}(a + c, b + c)$$

Finset.image_add_left_Icc theorem

(a b c : α) : (Icc a b).image (c + ·) = Icc (c + a) (c + b)

Full source

@[simp] lemma image_add_left_Icc (a b c : α) : (Icc a b).image (c + ·) = Icc (c + a) (c + b) := by
  rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Left Translation Preserves Closed Interval Finsets: $(c + \cdot) \text{``} [a, b] = [c + a, c + b]$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the closed interval finset $[a, b]$ under the left translation map $x \mapsto c + x$ is equal to the closed interval finset $[c + a, c + b]$. In symbols: $$(c + \cdot) \text{``} [a, b] = [c + a, c + b]$$

Finset.image_add_left_Ico theorem

(a b c : α) : (Ico a b).image (c + ·) = Ico (c + a) (c + b)

Full source

@[simp] lemma image_add_left_Ico (a b c : α) : (Ico a b).image (c + ·) = Ico (c + a) (c + b) := by
  rw [← map_add_left_Ico, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Left Translation Preserves Closed-Open Interval Finsets: $\text{Ico}(a, b) + c = \text{Ico}(a + c, b + c)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the closed-open interval finset $\text{Ico}(a, b)$ under the left translation map $x \mapsto c + x$ is equal to the closed-open interval finset $\text{Ico}(c + a, c + b)$. In symbols: $$\text{image}(x \mapsto c + x, \text{Ico}(a, b)) = \text{Ico}(c + a, c + b)$$

Finset.image_add_left_Ioc theorem

(a b c : α) : (Ioc a b).image (c + ·) = Ioc (c + a) (c + b)

Full source

@[simp] lemma image_add_left_Ioc (a b c : α) : (Ioc a b).image (c + ·) = Ioc (c + a) (c + b) := by
  rw [← map_add_left_Ioc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Left Addition Preserves Open-Closed Interval Finsets: $c + \text{Ioc}(a, b) = \text{Ioc}(c + a, c + b)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the open-closed interval finset $\text{Ioc}(a, b)$ under the left addition map $x \mapsto c + x$ is equal to the open-closed interval finset $\text{Ioc}(c + a, c + b)$. In symbols: $$\{c + x \mid x \in \text{Ioc}(a, b)\} = \text{Ioc}(c + a, c + b)$$

Finset.image_add_left_Ioo theorem

(a b c : α) : (Ioo a b).image (c + ·) = Ioo (c + a) (c + b)

Full source

@[simp] lemma image_add_left_Ioo (a b c : α) : (Ioo a b).image (c + ·) = Ioo (c + a) (c + b) := by
  rw [← map_add_left_Ioo, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Left Addition Preserves Open Interval Finsets: $c + \text{Ioo}(a, b) = \text{Ioo}(c + a, c + b)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the open interval finset $\text{Ioo}(a, b)$ under the left addition map $x \mapsto c + x$ is equal to the open interval finset $\text{Ioo}(c + a, c + b)$. In symbols: $$\text{image} (\lambda x, c + x) (\text{Ioo}(a, b)) = \text{Ioo}(c + a, c + b)$$

Finset.image_add_right_Icc theorem

(a b c : α) : (Icc a b).image (· + c) = Icc (a + c) (b + c)

Full source

@[simp] lemma image_add_right_Icc (a b c : α) : (Icc a b).image (· + c) = Icc (a + c) (b + c) := by
  rw [← map_add_right_Icc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Right Addition Preserves Closed Interval Finsets: $\text{Icc}(a, b) + c = \text{Icc}(a + c, b + c)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the closed interval finset $\text{Icc}(a, b)$ under the right addition map $x \mapsto x + c$ is equal to the closed interval finset $\text{Icc}(a + c, b + c)$. In symbols: $$\text{image} (\lambda x, x + c) (\text{Icc}(a, b)) = \text{Icc}(a + c, b + c)$$

Finset.image_add_right_Ico theorem

(a b c : α) : (Ico a b).image (· + c) = Ico (a + c) (b + c)

Full source

@[simp] lemma image_add_right_Ico (a b c : α) : (Ico a b).image (· + c) = Ico (a + c) (b + c) := by
  rw [← map_add_right_Ico, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Right Translation Preserves Closed-Open Intervals: $\text{Ico}(a, b) + c = \text{Ico}(a + c, b + c)$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the closed-open interval $[a, b)$ under the right translation map $x \mapsto x + c$ is the closed-open interval $[a + c, b + c)$. In other words, the finset obtained by applying the right translation by $c$ to each element of $\text{Ico}(a, b)$ is equal to the finset $\text{Ico}(a + c, b + c)$.

Finset.image_add_right_Ioc theorem

(a b c : α) : (Ioc a b).image (· + c) = Ioc (a + c) (b + c)

Full source

@[simp] lemma image_add_right_Ioc (a b c : α) : (Ioc a b).image (· + c) = Ioc (a + c) (b + c) := by
  rw [← map_add_right_Ioc, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Right Translation Preserves Open-Closed Interval: $(a, b] + c = (a + c, b + c]$

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the open-closed interval $(a, b]$ under the right translation map $x \mapsto x + c$ is equal to the open-closed interval $(a + c, b + c]$. That is, $$ \{x + c \mid x \in (a, b]\} = (a + c, b + c]. $$

Finset.image_add_right_Ioo theorem

(a b c : α) : (Ioo a b).image (· + c) = Ioo (a + c) (b + c)

Full source

@[simp] lemma image_add_right_Ioo (a b c : α) : (Ioo a b).image (· + c) = Ioo (a + c) (b + c) := by
  rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Right Translation Preserves Open Interval Finsets in Ordered Cancellative Additive Monoids

Informal description

Let $\alpha$ be an ordered cancellative additive monoid with a locally finite order. For any elements $a, b, c \in \alpha$, the image of the open interval finset $\text{Ioo}(a, b)$ under the right translation map $x \mapsto x + c$ is equal to the open interval finset $\text{Ioo}(a + c, b + c)$. In symbols: $$(\text{Ioo}(a, b)) + c = \text{Ioo}(a + c, b + c)$$