English
The image of an analytic set under a continuous map is analytic.
Русский
Образ аналитического множества под непрерывной картой аналитичен.
LaTeX
$$$AnalyticSet(s) \to \forall f: X \to Y, \text{ Continuous } f \Rightarrow AnalyticSet(f'' s).$$$
Lean4
/-- Given a Borel-measurable function from a Polish space to a second-countable space, there exists
a finer Polish topology on the source space for which the function is continuous. -/
theorem _root_.Measurable.exists_continuous {α β : Type*} [t : TopologicalSpace α] [PolishSpace α] [MeasurableSpace α]
[BorelSpace α] [tβ : TopologicalSpace β] [MeasurableSpace β] [OpensMeasurableSpace β] {f : α → β}
[SecondCountableTopology (range f)] (hf : Measurable f) :
∃ t' : TopologicalSpace α, t' ≤ t ∧ @Continuous α β t' tβ f ∧ @PolishSpace α t' :=
by
obtain ⟨b, b_count, -, hb⟩ : ∃ b : Set (Set (range f)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b :=
exists_countable_basis (range f)
haveI : Countable b := b_count.to_subtype
have : ∀ s : b, IsClopenable (rangeFactorization f ⁻¹' s) := fun s ↦
by
apply MeasurableSet.isClopenable
exact hf.subtype_mk (hb.isOpen s.2).measurableSet
choose T Tt Tpolish _ Topen using this
obtain ⟨t', t'T, t't, t'_polish⟩ : ∃ t' : TopologicalSpace α, (∀ i, t' ≤ T i) ∧ t' ≤ t ∧ @PolishSpace α t' :=
exists_polishSpace_forall_le (t := t) T Tt Tpolish
refine ⟨t', t't, ?_, t'_polish⟩
have : Continuous[t', _] (rangeFactorization f) := hb.continuous_iff.2 fun s hs => t'T ⟨s, hs⟩ _ (Topen ⟨s, hs⟩)
exact continuous_subtype_val.comp this
