English
A subset s of α is analytic if and only if there exists a Polish space β, a continuous map f: β → α, with range f = s.
Русский
Подмножество s пространства α аналитично тогда, когда существует полиш-пространство β и непрерывная отображение f: β → α с тем, что образ range f совпадает с s.
LaTeX
$$$AnalyticSet(s) \;\iff\; \exists \beta\; (h : TopologicalSpace \beta) \; (\_ : @PolishSpace \beta h)\; (f : \beta \to \alpha),\; @Continuous _ _ h _ f \wedge \operatorname{range} f = s$$$
Lean4
/-- A set is analytic if and only if it is the continuous image of some Polish space. -/
theorem analyticSet_iff_exists_polishSpace_range {s : Set α} :
AnalyticSet s ↔
∃ (β : Type) (h : TopologicalSpace β) (_ : @PolishSpace β h) (f : β → α), @Continuous _ _ h _ f ∧ range f = s :=
by
constructor
· intro h
rw [AnalyticSet] at h
rcases h with h | h
· refine ⟨Empty, inferInstance, inferInstance, Empty.elim, continuous_bot, ?_⟩
rw [h]
exact range_eq_empty _
· exact ⟨ℕ → ℕ, inferInstance, inferInstance, h⟩
· rintro ⟨β, h, h', f, f_cont, f_range⟩
rw [← f_range]
exact analyticSet_range_of_polishSpace f_cont
