English
The relative product of a family of homotopies between functions f_i and g_i, parameterized by i in I, yields a homotopy between the function pi f and pi g.
Русский
Относительное произведение семейства гомотопий между функциями f_i и g_i, параметризованное i∈I, задаёт гомотопию между функциями pi f и pi g.
LaTeX
$$$\mathrm{pi} (\{f_i\},\{g_i\}, S) : \mathrm{HomotopyRel}(\pi f, \pi g)\; S$$$
Lean4
/-- The relative product homotopy of `homotopies` between functions `f` and `g` -/
@[simps!]
def pi (homotopies : ∀ i : I, HomotopyRel (f i) (g i) S) : HomotopyRel (pi f) (pi g) S :=
{ Homotopy.pi fun i => (homotopies i).toHomotopy with
prop' := by
intro t x hx
dsimp only [coe_mk, pi_eval, toFun_eq_coe, HomotopyWith.coe_toContinuousMap]
simp only [funext_iff]
intro i
exact (homotopies i).prop' t x hx }
