image_of_continuous — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image_of_continuous {β : Type*} [TopologicalSpace β] {s : Set α} (hs : AnalyticSet s) {f : α → β}
    (hf : Continuous f) : AnalyticSet (f '' s) :=
  hs.image_of_continuousOn hf.continuousOn

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