English
The map sending (i, g) to (sigmaMk i).comp g is an embedding of the sigma-indexed product of continuous maps into a product of continuous maps.
Русский
Отображение, отправляющее (i, g) в (sigmaMk i) ∘ g, является вложением в соответствующий продукт непрерывных отображений.
LaTeX
$$$IsEmbedding\\ (\\\\lambda g: (\\\\sigmaMk g.fst).\\\\comp g.snd)$$$
Lean4
theorem isEmbedding_sigmaMk_comp [Nonempty X] : IsEmbedding (fun g : Σ i, C(X, Y i) ↦ (sigmaMk g.1).comp g.2)
where
toIsInducing :=
inducing_sigma.2
⟨fun i ↦ (sigmaMk i).isInducing_postcomp IsEmbedding.sigmaMk.isInducing, fun i ↦
let ⟨x⟩ := ‹Nonempty X›
⟨_, (isOpen_sigma_fst_preimage { i }).preimage (continuous_eval_const x), fun _ ↦ Iff.rfl⟩⟩
injective := by
rintro ⟨i, g⟩ ⟨i', g'⟩ h
obtain ⟨rfl, hg⟩ : i = i' ∧ ⇑g ≍ ⇑g' := Function.eq_of_sigmaMk_comp <| congr_arg DFunLike.coe h
simpa using hg
