English
If γ1: Path a1 a2 and γ2: Path b1 b2, their pointwise product γ1.prod γ2 is a path from (a1,b1) to (a2,b2) in the product space, given by t ↦ (γ1(t), γ2(t)).
Русский
Если γ1: Path a1 a2 и γ2: Path b1 b2, их попарное произведение γ1.prod γ2 — путь в произведении пространств от (a1,b1) до (a2,b2), заданный t ↦ (γ1(t), γ2(t)).
LaTeX
$$$\gamma_1.prod γ_2: Path (a_1,b_1) (a_2,b_2)$ with $(\gamma_1.prod γ_2)(t)=(\gamma_1(t),\gamma_2(t))$$$
Lean4
/-- Given a path in `X` and a path in `Y`, we can take their pointwise product to get a path in
`X × Y`. -/
protected def prod (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : Path (a₁, b₁) (a₂, b₂)
where
toContinuousMap := ContinuousMap.prodMk γ₁.toContinuousMap γ₂.toContinuousMap
source' := by simp
target' := by simp
