case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : X → Y
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hg : ‖g‖ = ‖compContinuous g (ContinuousMap.mk e)‖
⊢ ∃ g_1, ‖g_1‖ = ‖compContinuous g (ContinuousMap.mk e)‖ ∧ ↑g_1 ∘ e = ↑(compContinuous g (ContinuousMap.mk e))
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : X → Y
he : ClosedEmbedding e
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ ↑g ∘ e = ↑f
rcases exists_extension_norm_eq_of_closedEmbedding' f ⟨e, he.continuous⟩ he with ⟨g, hg, rfl⟩
no goals
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : X → Y
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hg : ‖g‖ = ‖compContinuous g (ContinuousMap.mk e)‖
⊢ ∃ g_1, ‖g_1‖ = ‖compContinuous g (ContinuousMap.mk e)‖ ∧ ↑g_1 ∘ e = ↑(compContinuous g (ContinuousMap.mk e))
exact ⟨g, hg, rfl⟩