English
If s ⊂ Πn E_n is closed, there exists a retraction from the product onto s that factors through the subtype inclusion.
Русский
Пусть s — замкнутое подмножество произведения Πn E_n. Тогда существует ретракция с произведения на s через включение в подраздел.
LaTeX
$$$$\\\\exists f:(\\\\forall n, E n)\\\\rightarrow s, \\\\forall x: s, f x = x \\\\land \\\\text{Surjective } f \\\\land \\\\text{Continuous } f.$$$$
Lean4
/-- Given a closed embedding into a Polish space, the source space is also Polish. -/
theorem _root_.Topology.IsClosedEmbedding.polishSpace [TopologicalSpace α] [TopologicalSpace β] [PolishSpace β]
{f : α → β} (hf : IsClosedEmbedding f) : PolishSpace α :=
by
letI := upgradeIsCompletelyMetrizable β
letI : MetricSpace α := hf.isEmbedding.comapMetricSpace f
haveI : SecondCountableTopology α := hf.isEmbedding.secondCountableTopology
have : CompleteSpace α :=
by
rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
exact hf.isClosed_range.isComplete
infer_instance
