prodMap — Mathlib

English

Let a family of maps f0 i, f1 i: X i → Y i have homotopies Fi for each i. Then the induced map piMap f0 to piMap f1 is homotopic via Fi composed with eval i.

Русский

Пусть для каждого i существуются отображения f0 i, f1 i: X i → Y i с гомотопиями Fi. Тогда piMap f0 и piMap f1 гомотопны через Fi ∘eval i.

LaTeX

$$$$ \text{piMap: } (\forall i, f_{0,i} \sim f_{1,i}) \Rightarrow \mathrm{Homotopic}(\pi f_0, \pi f_1) $$$$

Lean4

nonrec theorem prodMap {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Z, Z')} :
    Homotopic f₀ f₁ → Homotopic g₀ g₁ → Homotopic (f₀.prodMap g₀) (f₁.prodMap g₁)
  | ⟨F⟩, ⟨G⟩ => ⟨F.prodMap G⟩

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