trans_apply — Mathlib

English

The value of (F.trans G) at a point (t, x) is given by a piecewise formula using F on [0,1/2] and G on [1/2,1].

Русский

Значение (F.trans G) в точке (t, x) задаётся по кусочно-заданной формуле через F на [0,1/2] и G на [1/2,1].

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₀ f₁ f₂ : C(X, Y)} (F : HomotopyWith f₀ f₁ P) (G : HomotopyWith f₁ f₂ P) (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 _ _ _

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