instFunLike — Mathlib

English

If F is a Homotopy between f0 and f1 and G is a Homotopy between g0 and g1, then there exists a Homotopy F.prodMk G between f0.prodMk g0 and f1.prodMk g1.

Русский

Если F — гомотопия между f0 и f1 и G — между g0 и g1, то существует гомотопия F.prodMk G между f0.prodMk g0 и f1.prodMk g1.

LaTeX

$$$$ \text{prodMk: } (f_0 \sim f_1) \land (g_0 \sim g_1) \Rightarrow (f_0.prodMk g_0) \sim (f_1.prodMk g_1) $$$$

Lean4

instance instFunLike : FunLike (HomotopyWith f₀ f₁ P) (I × X) Y
    where
  coe F := ⇑F.toHomotopy
  coe_injective'
    | ⟨⟨⟨_, _⟩, _, _⟩, _⟩, ⟨⟨⟨_, _⟩, _, _⟩, _⟩, rfl => rfl

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