## 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 Iccs 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,

/-- 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
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)) :=

/-- 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