prodMk — Mathlib

English

If f0 ~ f1 and g0 ~ g1, then their product Mk is a Homotopy from f0.prodMk g0 to f1.prodMk g1.

Русский

Если f0 ~ f1 и g0 ~ g1, то их произведение Mk даёт гомотопию f0.prodMk g0 ~ f1.prodMk g1.

LaTeX

$$$$ f_0 \sim f_1 \Rightarrow g_0 \sim g_1 \Rightarrow (f_0.prodMk g_0) \sim (f_1.prodMk g_1) $$$$

Lean4

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

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