hcomp_apply — Mathlib

English

For the concatenation F.hcomp G, at the seam point (t, 1/2) the value is the middle vertex x1.

Русский

При разрезке конкатенации F.hcomp G на стыке t, 1/2 значение равно середине x1.

LaTeX

$$$F.hcomp G\,(t,\tfrac12) = x_1$$$

Lean4

theorem hcomp_apply (F : Homotopy p₀ q₀) (G : Homotopy p₁ q₁) (x : I × I) :
    F.hcomp G x =
      if h : (x.2 : ℝ) ≤ 1 / 2 then F.eval x.1 ⟨2 * x.2, (unitInterval.mul_pos_mem_iff zero_lt_two).2 ⟨x.2.2.1, h⟩⟩
      else G.eval x.1 ⟨2 * x.2 - 1, unitInterval.two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, x.2.2.2⟩⟩ :=
  show ite _ _ _ = _ by split_ifs <;> exact Path.extend_extends _ _

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