pi_lift — Mathlib

English

The quotient version of pi on a family of actual paths coincides with the pi on the quotient objects.

Русский

Квантообразная версия pi для реальных путей совпадает с pi на соответствующих объектах-коэффициентах.

LaTeX

$$$\mathrm{Path.Homotopic.pi\; fun\ i \mapsto \langle \gamma_i \rangle} = \langle \mathrm{Path.pi}\; \gamma \rangle$$$

Lean4

theorem pi_lift (γ : ∀ i, Path (as i) (bs i)) : (Path.Homotopic.pi fun i => ⟦γ i⟧) = ⟦Path.pi γ⟧ := by unfold pi; simp

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