pi_coe — Mathlib

English

The Pi-path is defined so that its coordinate map equals (γ_i(t)) at each i; in particular, the i-th projection of Path.pi γ is γ_i.

Русский

Путь через произведение определяется так, что его координатная карта равна (γ_i(t)) по каждой координате; проекция на i-й компоненту совпадает с γ_i.

LaTeX

$$$\bigl(\mathrm{Path.pi}\,\gamma\bigr)^{\wedge i}(t) = \gamma_i(t) \quad\text{for all } i, t.$$$

Lean4

@[simp]
theorem pi_coe (γ : ∀ i, Path (as i) (bs i)) : ⇑(Path.pi γ) = fun t i => γ i t :=
  rfl

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