α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s t : Set α
hs : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint s t
⊢ MeasurablySeparable s t
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s t : Set α
hs : AnalyticSet s
ht : AnalyticSet t
h : Disjoint s t
⊢ MeasurablySeparable s t
rw [AnalyticSet] at hs ht
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint ∅ t
⊢ MeasurablySeparable ∅ t

case inr.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) t
⊢ MeasurablySeparable (range f) t
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s t : Set α
hs : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint s t
⊢ MeasurablySeparable s t
rcases hs with (rfl | ⟨f, f_cont, rfl⟩)
case inr.intro.intro.inl
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) ∅
⊢ MeasurablySeparable (range f) ∅

case inr.intro.intro.inr.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
g : (ℕ → ℕ) → α
g_cont : Continuous g
h : Disjoint (range f) (range g)
⊢ MeasurablySeparable (range f) (range g)
case inr.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) t
⊢ MeasurablySeparable (range f) t
rcases ht with (rfl | ⟨g, g_cont, rfl⟩)
no goals
case inr.intro.intro.inr.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
g : (ℕ → ℕ) → α
g_cont : Continuous g
h : Disjoint (range f) (range g)
⊢ MeasurablySeparable (range f) (range g)
exact measurablySeparable_range_of_disjoint f_cont g_cont h
no goals
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint ∅ t
⊢ MeasurablySeparable ∅ t
refine' ⟨∅, Subset.refl _, by simp, MeasurableSet.empty⟩
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint ∅ t
⊢ Disjoint t ∅
simp
no goals
case inr.intro.intro.inl
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) ∅
⊢ MeasurablySeparable (range f) ∅
exact ⟨univ, subset_univ _, by simp, MeasurableSet.univ⟩
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
ι : Type ?u.86140
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) ∅
⊢ Disjoint ∅ univ
simp