Theorems · Theorem · general topology

PiNat.exists_retraction_of_isClosed

∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)}, IsClosed s → s.Nonempty → ∃ f, (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ Continuous f

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.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

1 results in Mathlib

Foundations

Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceDiscreteTopology