case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : IsEmpty X
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f

case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : Nonempty X
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
cases isEmpty_or_nonempty X
case inr.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : Nonempty X
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, ↑g y ∈ Icc (↑f x₁) (↑f x₂)
hgf : ↑g ∘ e = ↑f
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : Nonempty X
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
rcases exists_extension_forall_exists_le_ge_of_closedEmbedding f he with ⟨g, hg, hgf⟩
case inr.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : Nonempty X
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, ↑g y ∈ Icc (↑f x₁) (↑f x₂)
hgf : ↑g ∘ e = ↑f
y : Y
⊢ ↑g y ∈ t
case inr.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : Nonempty X
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, ↑g y ∈ Icc (↑f x₁) (↑f x₂)
hgf : ↑g ∘ e = ↑f
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
refine' ⟨g, fun y => _, hgf⟩
case inr.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : Nonempty X
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, ↑g y ∈ Icc (↑f x₁) (↑f x₂)
hgf : ↑g ∘ e = ↑f
y : Y
xl xu : X
h : ↑g y ∈ Icc (↑f xl) (↑f xu)
⊢ ↑g y ∈ t
case inr.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : Nonempty X
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, ↑g y ∈ Icc (↑f x₁) (↑f x₂)
hgf : ↑g ∘ e = ↑f
y : Y
⊢ ↑g y ∈ t
rcases hg y with ⟨xl, xu, h⟩
no goals
case inr.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : Nonempty X
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, ↑g y ∈ Icc (↑f x₁) (↑f x₂)
hgf : ↑g ∘ e = ↑f
y : Y
xl xu : X
h : ↑g y ∈ Icc (↑f xl) (↑f xu)
⊢ ↑g y ∈ t
exact hs.out (hf _) (hf _) h
case inl.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
he : ClosedEmbedding e
h✝ : IsEmpty X
c : ℝ
hc : c ∈ t
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h✝ : IsEmpty X
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
rcases hne with ⟨c, hc⟩
no goals
case inl.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
he : ClosedEmbedding e
h✝ : IsEmpty X
c : ℝ
hc : c ∈ t
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
refine' ⟨const Y c, fun _ => hc, funext fun x => isEmptyElim x⟩