image_of_continuousOn — Mathlib

English

If s ⊆ α is analytic and f: α → β is defined and continuous on s, then the image f''s is analytic.

Русский

Если s ⊆ α аналитично и f: α → β непрерывна на s, то образ f''s аналитичен.

LaTeX

$$$AnalyticSet(s) \rightarrow (f: \alpha \to \beta) \\text{ ContinuousOn } f\; s \Rightarrow \operatorname{AnalyticSet}(f'' s).$$$

Lean4

/-- The continuous image of an analytic set is analytic -/
theorem image_of_continuousOn {β : Type*} [TopologicalSpace β] {s : Set α} (hs : AnalyticSet s) {f : α → β}
    (hf : ContinuousOn f s) : AnalyticSet (f '' s) :=
  by
  rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨γ, γtop, γpolish, g, g_cont, gs⟩
  have : f '' s = range (f ∘ g) := by rw [range_comp, gs]
  rw [this]
  apply analyticSet_range_of_polishSpace
  apply hf.comp_continuous g_cont fun x => _
  rw [← gs]
  exact mem_range_self

Похожие утверждения