class IsAbsoluteNeighborhoodRetract (X : Type u_1) [TopologicalSpace X] : Prop

A topological space X is an absolute neighborhood retract (ANR) if, whenever it is embedded as a closed subspace of a normal space Y, there exists a continuous retraction from some open neighborhood of X in Y onto X.

More precisely, for every closed embedding e : X → Y into a normal space Y, there exist an open set U ⊆ Y containing the image of e and a continuous map r : Y → X defined on U such that r ∘ e = id.

• exists_neighborhood_retract (Y : Type u_2) [TopologicalSpace Y] [NormalSpace Y] (e : X → Y) : Topology.IsClosedEmbedding e → ∃ (U : Set Y) (r : Y → X), IsOpen U ∧ Set.range e ⊆ U ∧ ContinuousOn r U ∧ ∀ (x : X), r (e x) = x