case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
f : ((n : ℕ) → E n) → (n : ℕ) → E n
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
frange : range f = s
hf : LipschitzWith 1 f
⊢ ∃ f, (∀ (x : (n : ℕ) → E n), x ∈ s → f x = x) ∧ range f = s ∧ Continuous f
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
⊢ ∃ f, (∀ (x : (n : ℕ) → E n), x ∈ s → f x = x) ∧ range f = s ∧ Continuous f
rcases exists_lipschitz_retraction_of_isClosed hs hne with ⟨f, fs, frange, hf⟩
no goals
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : Set.Nonempty s
f : ((n : ℕ) → E n) → (n : ℕ) → E n
fs : ∀ (x : (n : ℕ) → E n), x ∈ s → f x = x
frange : range f = s
hf : LipschitzWith 1 f
⊢ ∃ f, (∀ (x : (n : ℕ) → E n), x ∈ s → f x = x) ∧ range f = s ∧ Continuous f
exact ⟨f, fs, frange, hf.continuous⟩