prod_coe — Mathlib

English

The underlying function of γ1.prod γ2 is the product of the underlying functions: ⇑(γ1.prod γ2) = (t ↦ (γ1 t, γ2 t)).

Русский

Базовая функция γ1.prod γ2 — это попарное произведение базовых функций: (γ1.prod γ2)(t) = (γ1(t), γ2(t)).

LaTeX

$$$\big(\gamma_1.prod \gamma_2\big)^{\;\;}(t) = (\gamma_1(t), \gamma_2(t))$$$

Lean4

@[simp]
theorem prod_coe (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : ⇑(γ₁.prod γ₂) = fun t => (γ₁ t, γ₂ t) :=
  rfl

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