English
For a family of spaces (βi) indexed by i, the coordinate update map updating the i-th coordinate is a closed embedding.
Русский
Для семейства пространств (βi), индексируемого i, отображение обновления координаты i является замкнутым вложением.
LaTeX
$$$ \\text{IsClosedEmbedding}(\\mathrm{update}\\, x\\, i). $$$
Lean4
theorem isClosedEmbedding_update {ι : Type*} {β : ι → Type*} [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)]
(x : (i : ι) → β i) (i : ι) [(i : ι) → T1Space (β i)] : IsClosedEmbedding (update x i) :=
by
refine
.of_continuous_injective_isClosedMap (continuous_const.update i continuous_id) (update_injective x i) fun s hs ↦ ?_
rw [update_image]
apply isClosed_set_pi
simp [forall_update_iff, hs]
