Lebesgue number lemma for paths?

Stream: Is there code for X?

[Kim Morrison]

Does anyone have:

import Mathlib

theorem Path.exists_partition_in_cover {X : Type*} [TopologicalSpace X]
    {ι : Type*} (U : ι → Set X) (hU_open : ∀ i, IsOpen (U i))
    {x y : X} (γ : Path x y) (hU_cover : Set.range γ ⊆ ⋃ i, U i) :
    ∃ (n : ℕ) (t : Fin (n + 1) → unitInterval),
      StrictMono t ∧ t 0 = 0 ∧ t (Fin.last n) = 1 ∧
      (∀ i : Fin n, ∃ j : ι,
        ∀ s : unitInterval, (t i.castSucc : ℝ) ≤ s ∧ s ≤ (t i.succ : ℝ) → γ s ∈ U j) := by
  sorry

[Joël Riou]

Just in case, it should follow easily from docs#lebesgue_number_lemma_of_metric

[Kim Morrison]

Ah, just found docs#exists_monotone_Icc_subset_open_cover_unitInterval

[Kim Morrison]

Slight impedance mismatch with Nat/Fin and Monotone/StrictMono, I might just provide variants.