extend_trans_of_half_le — Mathlib

English

If t ≥ 1/2, then the extension equals the second path extended by 2t−1.

Русский

Если t ≥ 1/2, продолжение равно γ2.extend(2t−1).

LaTeX

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

Lean4

theorem extend_trans_of_half_le (γ₁ : Path x y) (γ₂ : Path y z) {t : ℝ} (ht : 1 / 2 ≤ t) :
    (γ₁.trans γ₂).extend t = γ₂.extend (2 * t - 1) :=
  by
  conv_lhs => rw [← sub_sub_cancel 1 t]
  rw [← extend_symm_apply, trans_symm, extend_trans_of_le_half _ _ (by linarith), extend_symm_apply]
  congr 1
  linarith

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