analyticSet_image — Mathlib

English

If s is an open subset of a Polish space β and f: β → α is continuous, then the image f''s is analytic in α.

Русский

Если s открытое подмножество полишевского пространства β и f: β → α непрерывна, то образ f''s является аналитическим в α.

LaTeX

$$$IsOpen(s) \\&\; f: \beta \to \alpha \; (\text{Continuous } f) \Rightarrow \operatorname{AnalyticSet}(f'' s).$$$

Lean4

/-- The image of an open set under a continuous map is analytic. -/
theorem _root_.IsOpen.analyticSet_image {β : Type*} [TopologicalSpace β] [PolishSpace β] {s : Set β} (hs : IsOpen s)
    {f : β → α} (f_cont : Continuous f) : AnalyticSet (f '' s) :=
  by
  rw [image_eq_range]
  haveI : PolishSpace s := hs.polishSpace
  exact analyticSet_range_of_polishSpace (f_cont.comp continuous_subtype_val)

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