English
A family of paths (γ_i) in each X_i induces a path in the product space ∏i X_i by taking coordinatewise values: Path.pi γ is a path from (a_i) to (b_i) with (Path.pi γ)(t) = (γ_i(t))_i.
Русский
Семейство путей (γ_i) в пространствах X_i порождает путь в произведении ∏i X_i, координатно: (Path.pi γ)(t) = (γ_i(t))_i.
LaTeX
$$$\text{Path.pi}\,\gamma$ is a path from $(a_i)_{i}$ to $(b_i)_{i}$ in $\prod_i X_i$ with $\bigl(\text{Path.pi}\,\gamma\bigr)(t) = (\gamma_i(t))_i$ for all $t$.$$
Lean4
/-- Given a family of paths, one in each Xᵢ, we take their pointwise product to get a path in
Π i, Xᵢ. -/
protected def pi (γ : ∀ i, Path (as i) (bs i)) : Path as bs
where
toContinuousMap := ContinuousMap.pi fun i => (γ i).toContinuousMap
source' := by simp
target' := by simp
