Theorems · Theorem · general topology

PiNat.exists_lipschitz_retraction_of_isClosed

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

Given a closed nonempty subset s of Π (n : ℕ), E n, there exists a Lipschitz retraction onto this set, i.e., a Lipschitz map with range equal to s, equal to the identity on s.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDiscreteTopology