English
Let β be a Polish space and α a topological space. If f: β → α is continuous, then the image of β under f, i.e. range(f), is an analytic subset of α.
Русский
Пусть β — полишевое пространство, α — топологическое пространство. Если f: β → α непрерывна, то множество образа range(f) является аналитическим подмножеством α.
LaTeX
$$$\forall \beta,\; (\text{PolishSpace }\beta)\; \forall f: \beta \to \alpha,\; \text{Continuous } f \Rightarrow \operatorname{AnalyticSet}(\operatorname{range} f).$$$
Lean4
theorem analyticSet_range_of_polishSpace {β : Type*} [TopologicalSpace β] [PolishSpace β] {f : β → α}
(f_cont : Continuous f) : AnalyticSet (range f) :=
by
cases isEmpty_or_nonempty β
· rw [range_eq_empty]
exact analyticSet_empty
· rw [AnalyticSet]
obtain ⟨g, g_cont, hg⟩ : ∃ g : (ℕ → ℕ) → β, Continuous g ∧ Surjective g := exists_nat_nat_continuous_surjective β
refine Or.inr ⟨f ∘ g, f_cont.comp g_cont, ?_⟩
rw [hg.range_comp]
