English
Let s be a closed nonempty subset of the product space Πn E_n, with each E_n discrete topology. Then there exists a continuous map f: Πn E_n → Πn E_n with range f = s and f(x)=x for all x∈s.
Русский
Пусть s — замкнутое ненулевое подмножество произведения Πn E_n, где каждое E_n дискретно. Тогда существует непрерывное отображение f: Πn E_n → Πn E_n такое, что образ f равен s и f(x)=x для всех x∈s.
LaTeX
$$$\\\\exists f:(\\\\forall n, E n) \\\\to (\\\\forall n, E n), \\\\left( \\\\forall x \\\\in s, f x = x \\\\right) \\\\land \\\\text{range } f = s \\\\land \\\\text{Continuous } f$$$
Lean4
/-- Given a closed nonempty subset `s` of `Π (n : ℕ), E n`, there exists a retraction onto this
set, i.e., a continuous map with range equal to `s`, equal to the identity on `s`. -/
theorem exists_retraction_of_isClosed {s : Set (∀ n, E n)} (hs : IsClosed s) (hne : s.Nonempty) :
∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f :=
by
rcases exists_lipschitz_retraction_of_isClosed hs hne with ⟨f, fs, frange, hf⟩
exact ⟨f, fs, frange, hf.continuous⟩
