case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
⊢ AnalyticSet (f '' s)
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
⊢ AnalyticSet (f '' s)
rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨γ, γtop, γpolish, g, g_cont, gs⟩
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
⊢ AnalyticSet (f '' s)
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
⊢ AnalyticSet (f '' s)
skip
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (f '' s)
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
⊢ AnalyticSet (f '' s)
have : f '' s = range (f ∘ g) := by rw [range_comp, gs]
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (range (f ∘ g))
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (f '' s)
rw [this]
case intro.intro.intro.intro.intro.f_cont
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ Continuous (f ∘ g)
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (range (f ∘ g))
apply analyticSet_range_of_polishSpace
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ ∀ (x : γ), g x ∈ s
case intro.intro.intro.intro.intro.f_cont
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ Continuous (f ∘ g)
apply hf.comp_continuous g_cont fun x => _
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ ∀ (x : γ), g x ∈ range g
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ ∀ (x : γ), g x ∈ s
rw [← gs]
no goals
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ ∀ (x : γ), g x ∈ range g
exact mem_range_self
no goals
α : Type u_2
inst✝¹ : TopologicalSpace α
ι : Type ?u.3371
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous g
gs : range g = s
⊢ f '' s = range (f ∘ g)
rw [range_comp, gs]