case mp
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
⊢ AnalyticSet s → ∃ β h x f, Continuous f ∧ range f = s

case mpr
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
⊢ (∃ β h x f, Continuous f ∧ range f = s) → AnalyticSet s
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
⊢ AnalyticSet s ↔ ∃ β h x f, Continuous f ∧ range f = s
constructor
case mp
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : AnalyticSet s
⊢ ∃ β h x f, Continuous f ∧ range f = s
case mp
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
⊢ AnalyticSet s → ∃ β h x f, Continuous f ∧ range f = s
intro h
case mp
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s
⊢ ∃ β h x f, Continuous f ∧ range f = s
case mp
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : AnalyticSet s
⊢ ∃ β h x f, Continuous f ∧ range f = s
rw [AnalyticSet] at h
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : s = ∅
⊢ ∃ β h x f, Continuous f ∧ range f = s

case mp.inr
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : ∃ f, Continuous f ∧ range f = s
⊢ ∃ β h x f, Continuous f ∧ range f = s
case mp
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s
⊢ ∃ β h x f, Continuous f ∧ range f = s
cases' h with h h
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : s = ∅
⊢ range Empty.elim = s
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : s = ∅
⊢ ∃ β h x f, Continuous f ∧ range f = s
refine' ⟨Empty, inferInstance, inferInstance, Empty.elim, continuous_bot, _⟩
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : s = ∅
⊢ range Empty.elim = ∅
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : s = ∅
⊢ range Empty.elim = s
rw [h]
no goals
case mp.inl
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : s = ∅
⊢ range Empty.elim = ∅
exact range_eq_empty _
no goals
case mp.inr
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
h : ∃ f, Continuous f ∧ range f = s
⊢ ∃ β h x f, Continuous f ∧ range f = s
exact ⟨ℕ → ℕ, inferInstance, inferInstance, h⟩
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet s
case mpr
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
⊢ (∃ β h x f, Continuous f ∧ range f = s) → AnalyticSet s
rintro ⟨β, h, h', f, f_cont, f_range⟩
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet s
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet s
skip
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet (range f)
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet s
rw [← f_range]
no goals
case mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
ι : Type ?u.2204
s : Set α
β : Type
h : TopologicalSpace β
h' : PolishSpace β
f : β → α
f_cont : Continuous f
f_range : range f = s
⊢ AnalyticSet (range f)
exact analyticSet_range_of_polishSpace f_cont