English
The coinducingCoprod maps yield continuous dependence: for S, x in X(S), the map a ↦ coinducingCoprod⟨⟨S, x⟩, a⟩ is continuous in a, and thus continuous in each fiber.
Русский
Копридвижные копродукты дают непрерывную зависимость: для S и x в X(S) отображение a ↦ coinducingCoprod⟨⟨S, x⟩, a⟩ непрерывно по a, и по отдельным фибрам.
LaTeX
$$$\forall S:\mathrm{CompHaus},\; x\in X(S),\; \mathrm{Continuous}(a \mapsto \mathrm{coinducingCoprod}\langle\langle S, x\rangle, a\rangle)$$$
Lean4
theorem continuous_coinducingCoprod {S : CompHaus.{u}} (x : X.val.obj ⟨S⟩) :
Continuous fun a ↦ (X.coinducingCoprod ⟨⟨S, x⟩, a⟩) :=
by
suffices ∀ (i : (T : CompHaus.{u}) × X.val.obj ⟨T⟩), Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from
this ⟨_, _⟩
rw [← continuous_sigma_iff]
apply continuous_coinduced_rng
