trans_apply — Mathlib

English

The glued relative homotopy (F trans G) acts by F on the first half and by G on the second half, with a precise reparametrization.

Русский

Склеенная относительная гомотопия действует как F на первой половине и как G на второй половине, с точной перераспределением параметров.

LaTeX

$$$(F\trans G)(t,x) = \begin{cases}F(2t,x), & t\le 1/2, \\ G(2t-1,x), & t>1/2.\end{cases}$$$

Lean4

theorem trans_apply (F : HomotopyRel f₀ f₁ S) (G : HomotopyRel f₁ f₂ S) (x : I × X) :
    (F.trans G) x =
      if h : (x.1 : ℝ) ≤ 1 / 2 then F (⟨2 * x.1, (unitInterval.mul_pos_mem_iff zero_lt_two).2 ⟨x.1.2.1, h⟩⟩, x.2)
      else G (⟨2 * x.1 - 1, unitInterval.two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, x.1.2.2⟩⟩, x.2) :=
  Homotopy.trans_apply _ _ _

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