case inl
α : Type u
β : Type v
ι : Type ?u.150118
π : ι → Type ?u.150123
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hne : Set.Nonempty T
hS : IsPreconnected ∅
hc : ContinuousOn f ∅
hTm : MapsTo f ∅ T
⊢ ∃ y, y ∈ T ∧ EqOn f (const α y) ∅

case inr.intro
α : Type u
β : Type v
ι : Type ?u.150118
π : ι → Type ?u.150123
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : Set.Nonempty T
x : α
hx : x ∈ S
⊢ ∃ y, y ∈ T ∧ EqOn f (const α y) S
α : Type u
β : Type v
ι : Type ?u.150118
π : ι → Type ?u.150123
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : Set.Nonempty T
⊢ ∃ y, y ∈ T ∧ EqOn f (const α y) S
rcases S.eq_empty_or_nonempty with (rfl | ⟨x, hx⟩)
no goals
case inl
α : Type u
β : Type v
ι : Type ?u.150118
π : ι → Type ?u.150123
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hne : Set.Nonempty T
hS : IsPreconnected ∅
hc : ContinuousOn f ∅
hTm : MapsTo f ∅ T
⊢ ∃ y, y ∈ T ∧ EqOn f (const α y) ∅
exact hne.imp fun _ hy => ⟨hy, eqOn_empty _ _⟩
no goals
case inr.intro
α : Type u
β : Type v
ι : Type ?u.150118
π : ι → Type ?u.150123
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : Set.Nonempty T
x : α
hx : x ∈ S
⊢ ∃ y, y ∈ T ∧ EqOn f (const α y) S
exact ⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hc hTm hx' hx⟩