extend_trans_of_le_half — Mathlib

English

If t ≤ 1/2, then the extension of the concatenation equals the first path extended by 2t.

Русский

Если t ≤ 1/2, продолжение конкатенации равно γ1.extend(2t).

LaTeX

$$$ (\gamma_1.\text{trans } \gamma_2).\extend t = \gamma_1.\extend (2t) \quad\text{for } t \le \tfrac12$$$

Lean4

theorem extend_trans_of_le_half (γ₁ : Path x y) (γ₂ : Path y z) {t : ℝ} (ht : t ≤ 1 / 2) :
    (γ₁.trans γ₂).extend t = γ₁.extend (2 * t) :=
  by
  obtain _ | ht₀ := le_total t 0
  · repeat rw [extend_of_le_zero _ (by linarith)]
  · rwa [extend_extends _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_extends]

Похожие утверждения