Endpoint correction for time changes

An increasing continuous map can be kept up to an interior point and continued affinely so that the terminal endpoint is fixed.

theorem BGW.Skorokhod.exists_endpoint_timeChange {a r : ℝ} (hr : 0 ≤ r) (hra : r < a) (h : ↑(Set.Icc 0 a) → ℝ) (hc : Continuous h) (hm : StrictMono h) (h₀ : h ⟨0, ⋯⟩ = 0) (hᵣ : h ⟨r, ⋯⟩ < a) : ∃ (τ : TimeChange a), (∀ (t : ↑(Set.Icc 0 a)), ↑t ≤ r → ↑(τ t) = h t) ∧ ∀ (t : ↑(Set.Icc 0 a)), r ≤ ↑t → h ⟨r, ⋯⟩ ≤ ↑(τ t)

Correct the endpoint of an increasing continuous map by an affine final segment.