English
Let s ⊂ Πn E_n be closed and nonempty. There exists a continuous surjection f: Πn E_n → s which fixes all points of s (i.e., f|s = id on s).
Русский
Пусть s ⊂ Πn E_n замкнуто и не пусто. Существует непрерывное отображение f: Πn E_n → s, которое фиксирует все точки s (то есть f|s = id).
LaTeX
$$$\\\\exists f:(\\\\forall n, E n) \\\\to s, \\\\left( \\\\forall x: s, f x = x \\\\right) \\\\land \\\\text{Surjective } f \\\\land \\\\text{Continuous } f$$$
Lean4
theorem exists_retraction_subtype_of_isClosed {s : Set (∀ n, E n)} (hs : IsClosed s) (hne : s.Nonempty) :
∃ f : (∀ n, E n) → s, (∀ x : s, f x = x) ∧ Surjective f ∧ Continuous f :=
by
obtain ⟨f, fs, rfl, f_cont⟩ : ∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f :=
exists_retraction_of_isClosed hs hne
have A : ∀ x : range f, rangeFactorization f x = x := fun x ↦ Subtype.eq <| fs x x.2
exact ⟨rangeFactorization f, A, fun x => ⟨x, A x⟩, f_cont.subtype_mk _⟩
