case inl
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
h✝ : IsEmpty α
⊢ StronglyMeasurable f

case inr
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
h : Nonempty α
⊢ StronglyMeasurable f
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
⊢ StronglyMeasurable f
cases' isEmpty_or_nonempty α with _ h
no goals
case inl
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
h✝ : IsEmpty α
⊢ StronglyMeasurable f
exact stronglyMeasurable_of_isEmpty f
case h.e'_5
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
h : Nonempty α
⊢ f = fun x => ?inr.convert_3

case inr.convert_3
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
h : Nonempty α
⊢ β
case inr
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
h : Nonempty α
⊢ StronglyMeasurable f
convert stronglyMeasurable_const (β := β) using 1
no goals
case h.e'_5
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
h : Nonempty α
⊢ f = fun x => ?inr.convert_3

case inr.convert_3
α✝ : Type ?u.15025
β✝ : Type ?u.15028
γ : Type ?u.15031
ι : Type ?u.15034
inst✝¹ : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
h : Nonempty α
⊢ β
exact funext fun x => hf x h.some