exists interval containing two points

Stream: Is there code for X?

[Winston Yin (尹維晨)]

I've found a need for the following lemma:

example (t : ℝ) : ∃ T > 0, t ∈ Ioo (t₀ - T) (t₀ + T) := by
  refine ⟨2 * |t - t₀| + 1, by positivity, ?_⟩
  by_cases ht : t - t₀ < 0
  · rw [abs_of_neg ht]
    constructor <;> linarith
  · rw [abs_of_nonneg (not_lt.mp ht)]
    constructor <;> linarith

1. Does it exist in mathlib in some form?
2. If not, what's the best place to put it?
3. Should it be stated more generally, e.g. for rationals, metric spaces, etc.?

[Matt Diamond]

I don't have any answers, but just wanted to note that you could do |t - t₀| + 1 instead of 2 * |t - t₀| + 1

[Junyan Xu]

shorter:

import Mathlib.Topology.MetricSpace.PseudoMetric
example (t : ℝ) : ∃ T > 0, t ∈ Set.Ioo (t₀ - T) (t₀ + T) := by
  simp_rw [← Real.ball_eq_Ioo, Metric.mem_ball]
  exact ⟨|t - t₀| + 1, by positivity, lt_add_of_pos_right _ zero_lt_one⟩

[Winston Yin (尹維晨)]

Where should such a lemma be located? What about versions for rationals and Euclidean spaces?

[Junyan Xu]

We have docs#Int.ball_eq_Ioo but not Rat.ball_eq_Ioo. For general metric space, what should be the statement? We have docs#BoundedSpace and I recall seeing some discussion about the unbounded counterpart, but I can't find that now.

One generalization is the following:

import Mathlib.Data.Set.Intervals.Group
variable {α} [LinearOrderedAddCommGroup α]

theorem mem_Ioo_iff_abs_le {x y z : α} : |x - y| < z ↔ y ∈ Set.Ioo (x - z) (x + z) :=
  abs_lt.trans <| and_comm.trans <| and_congr sub_lt_comm neg_lt_sub_iff_lt_add'

example [Nontrivial α] (t₀ t : α) :
    ∃ T > 0, t ∈ Set.Ioo (t₀ - T) (t₀ + T) := by
  have ⟨ε, hε⟩ := exists_zero_lt (α := α)
  refine ⟨|t₀ - t| + ε, add_pos_of_nonneg_of_pos (abs_nonneg _) hε,
    mem_Ioo_iff_abs_le.mp (lt_add_of_pos_right _ hε)⟩

and it could go into the imported file. Actually you ported that file and there's a call for more API about symmetric intervals just above the lemma.

[Yaël Dillies]

Do you know about docs#HasSolidNorm ?

[Winston Yin (尹維晨)]

@Yaël Dillies could you clarify how this should help?

[Winston Yin (尹維晨)]

@Junyan Xu At least for Euclidean space, the generalisation from the reals is that there exists a ball around a that also contains b.

I do remember porting that file. Though I find the API around intervals generally lacking, I always hesitate to add anything because it usually means an explosion of lemmas for Ioo, Icc, Ioc, etc.

[Yaël Dillies]

Winston Yin (尹維晨) said:

Yaël Dillies could you clarify how this should help?

I don't know. But this is one way of relating the absolute value and the norm.

[Yaël Dillies]

What's the use case of your lemma? Do you need the interval to be centered?

[Yaël Dillies]

I'm asking because this is a bit of a weird lemma.

[Notification Bot]

Kamila Szewczyk has marked this topic as resolved.

[Kamila Szewczyk]

Notification Bot said:

Kamila Szewczyk has marked this topic as resolved.

Sorry! I was trying to move to a different topic, i am not very good with zulip.

[Notification Bot]

Kamila Szewczyk has marked this topic as unresolved.