# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: intervals, abs and shifts

#### Damiano Testa (Dec 17 2020 at 07:17):

In the course of reviewing a PR (#5361), I needed the lemmas below. Do they already appear? What would be a good home? As I have not used very much the side of mathlib with `Icc`

s and the like, I do not really know where they could go.

Any suggestions would be very much appreciated!

```
/-- A lemma relating a compact interval and its shifts. -/
lemma sub_mem_Icc_iff (α i y : ℝ) : (y - α ∈ Icc (- i) i ↔ y ∈ Icc (α - i) (α + i)) :=
⟨λ a,
⟨sub_le_iff_le_add.mpr (neg_le_sub_iff_le_add.mp a.1), sub_le_iff_le_add.mp (sub_le.mpr a.2)⟩,
λ a, ⟨neg_le_sub_iff_le_add.mpr (sub_le_iff_le_add.mp a.1) , sub_le_iff_le_add'.mpr a.2⟩⟩
/-- A lemma describing a compact interval via absolute values. -/
lemma abs_le_iff_mem_Icc (α i y : ℝ) : (abs (y - α) ≤ i ↔ y ∈ Icc (α - i) (α + i)) :=
⟨λ h, ⟨sub_le_of_abs_sub_le_left h, sub_le_iff_le_add'.mp (abs_le.mp h).2⟩,
λ h, abs_le.mpr ((sub_mem_Icc_iff α i y).mpr h)⟩
/-- An element of an open interval is closer to the left end-point than
the length of the interval. -/
lemma abs_lt_abs_left {a b c : ℝ} (hc : b ∈ Ioo a c) :
abs (a - b) < abs (a - c) :=
begin
rw [abs_lt, neg_lt, lt_abs, lt_abs, neg_sub, neg_sub],
exact ⟨or.inr (sub_lt_sub_right hc.2 a), or.inr (sub_lt_sub (lt_trans hc.1 hc.2) hc.1)⟩,
end
/-- An element of an open interval is closer to the right end-point than
the length of the interval. -/
lemma abs_lt_abs_right {a b c : ℝ} (hc : b ∈ Ioo a c) :
abs (c - b) < abs (a - c) :=
begin
rw [abs_sub, sub_eq_neg_add, sub_eq_neg_add, ← neg_neg b, ← neg_neg a],
exact abs_lt_abs_left ⟨neg_lt_neg_iff.mpr hc.2, neg_lt_neg_iff.mpr hc.1⟩,
end
```

#### Ruben Van de Velde (Dec 17 2020 at 19:11):

Is there any reason to use `Icc (- i) i`

instead of an arbitrary `Icc`

in the first lemma?

#### Damiano Testa (Dec 17 2020 at 19:29):

No real reason other than a lot of the arguments use "symmetric" intervals. I can definitely change this with virtually no effort!

#### Damiano Testa (Dec 18 2020 at 06:10):

Below are a version of the first lemma above, with arbitrary endpoints and a proof of the symmetric one as a consequence.

Is there a preference between the `simp only`

proof and the term mode proof in `sub_mem_Icc_iff`

?

```
/-- A lemma relating a compact interval and its shifts. -/
lemma sub_mem_Icc_iff (x y l m : ℝ) : (x - y ∈ Icc l m ↔ x ∈ Icc (y + l) (y + m)) :=
by simp only [le_sub_iff_add_le', sub_le_iff_le_add', iff_self, mem_Icc]
--⟨λ a, ⟨le_sub_iff_add_le'.mp a.1, sub_le_iff_le_add'.mp a.2⟩,
-- λ b, ⟨le_sub_iff_add_le'.mpr b.1, sub_le_iff_le_add'.mpr b.2⟩⟩
/-- A lemma relating a symmetric compact interval and its shifts. -/
lemma sub_mem_Icc_iff_symmetric (x y z : ℝ) : (x - y ∈ Icc (- z) z ↔ x ∈ Icc (y - z) (y + z)) :=
by rw [sub_mem_Icc_iff, tactic.ring.add_neg_eq_sub y z]
```

#### Eric Wieser (Dec 18 2020 at 09:24):

The statement of the former would seem more natural to me with the + terms on the right commuted

#### Damiano Testa (Dec 18 2020 at 09:25):

You mean `lemma sub_mem_Icc_iff (x y l m : ℝ) : (x - y ∈ Icc l m ↔ x ∈ Icc (l + y) (m + y))`

?

#### Eric Wieser (Dec 18 2020 at 09:26):

Also I'm surprised `add_neg_eq_sub`

is hidden away in `tactic.ring`

as docs#tactic.ring.add_neg_eq_sub. is there a more public name?

#### Damiano Testa (Dec 18 2020 at 09:27):

I was also surprised by this, but I could not find it and `library_search`

gave me... that!

#### Johan Commelin (Dec 18 2020 at 09:28):

`sub_eq_add_neg`

#### Eric Wieser (Dec 18 2020 at 09:36):

Reassuringly the `ring`

one is just written in terms of that one

Last updated: May 07 2021 at 19:12 UTC