Balls are OrdConnected

Stream: Is there code for X?

[Vincent Beffara]

Is this result hidden in Mathlib under a different name?

import Mathlib

theorem key {t u : (Set.Icc (0:ℝ) 1)} {ε : ℝ} (hε : ε > 0) (hu : u ∈ Metric.ball t ε) :
    Set.uIcc t u ⊆ Metric.ball t ε := by
  sorry

[Patrick Massot]

I cannot get something more direct than

import Mathlib

theorem key {t u : ℝ} {ε : ℝ} (hε : ε > 0) (hu : u ∈ Metric.ball t ε) :
    Set.uIcc t u ⊆ Metric.ball t ε := by
  have : Convex ℝ (Metric.ball t ε) := by
    exact? says exact convex_ball t ε
  rw [← segment_eq_uIcc]
  apply? says refine Convex.segment_subset this ?hx hu
  exact? says exact Metric.mem_ball_self hε

[Patrick Massot]

Note that rw? does not work because it is limited to 20 suggestions.

[Scott Morrison]

Should I remove the limit? rw? has the automatic "stop before you run out of heartbeats" mechanism, so perhaps the limit is just inconvenient.

[Scott Morrison]

#7741 sets it to 200, but I will take any suggestions. :-)

[Patrick Massot]

I don't know. In the example above it would be nice to say that your suggestion tactics find everything that is needed. But I don't think I would have had the patience to read 200 suggestions. I used the good old file browsing method.

[Yaël Dillies]

import Mathlib.Analysis.Convex.Normed

open Metric

theorem key {t u : ℝ} {ε : ℝ} (hε : ε > 0) (hu : u ∈ ball t ε) : Set.uIcc t u ⊆ ball t ε := by
  simpa only [segment_eq_uIcc] using (convex_ball t ε).segment_subset (mem_ball_self hε) hu

[Yaël Dillies]

Note that we don't have a convenient typeclass for "balls are order-connected" yet. It's annoying for what I do as well.

[Vincent Beffara]

Thanks - but in my question u and t are in a subtype, so I cannot use convexity which is why I was asking ...

[Yaël Dillies]

Yeah so that falls back onto "We don't have a convenient typeclass for "balls are order-connected" and Yaël is sad :sad:".

[Yaël Dillies]

But also Icc 0 1 is a convex space, just not to mathlib's definition. If you want a few months for me to perform the convexity refactor, this should Just Work.

[Vincent Beffara]

I will just get out of the Icc, prove inclusion in R and project back, I was just lazy to do that and was looking for a cool name saying that val is an order isomorphism or something to do it in one line

[Vincent Beffara]

OK apply is doing something that I don't really understand here but I'm happy anyway:

import Mathlib

open Set Metric

theorem key {t u : (Set.Icc (0:ℝ) 1)} {ε : ℝ} (hε : ε > 0) (hu : u ∈ Metric.ball t ε) :
    Set.uIcc t u ⊆ Metric.ball t ε := by
  suffices : uIcc t.1 u.1 ⊆ ball t.1 ε
  · intro v ; apply this
  simpa only [segment_eq_uIcc] using (convex_ball t.1 ε).segment_subset (mem_ball_self hε) hu

[Ruben Van de Velde]

That's because s ⊆ t is defined as ∀ x, x ∈ s → x ∈ t

[Ruben Van de Velde]

(Assuming I got the direction right)

[Vincent Beffara]

Yes I get this, what I wasn't predicting is how it sees through Subtype.val (although, v \in ball t e \iff v.1 \in ball t.1 e is rfl). I just tried apply because I was feeling lucky ;-)

[Ruben Van de Velde]

Though here apply is also seeing through the definition of some coercions. You can see a bit more of what's going on with

import Mathlib

open Set Metric

theorem key {t u : (Set.Icc (0:ℝ) 1)} {ε : ℝ} (hε : ε > 0) (hu : u ∈ Metric.ball t ε) :
    Set.uIcc t u ⊆ Metric.ball t ε := by
  suffices uIcc t.1 u.1 ⊆ ball t.1 ε by
    intro v
    rw [subset_def] at this
    specialize this v
    apply this
  simpa only [segment_eq_uIcc] using (convex_ball t.1 ε).segment_subset (mem_ball_self hε) hu

[Ruben Van de Velde]

This feels like something that should be covered by simp or norm_cast. (norm_cast finishes here, but only accidentally)