preimage — Mathlib

English

The preimage of an analytic set under a continuous map is analytic.

Русский

Прообраз аналитического множества под непрерывной картой аналитичен.

LaTeX

$$$AnalyticSet(s) \Rightarrow \forall f: X \to Y, \text{ Continuous } f \Rightarrow AnalyticSet(f^{-1}(s)).$$$

Lean4

/-- Preimage of an analytic set is an analytic set. -/
protected theorem preimage {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [PolishSpace X] [T2Space Y]
    {s : Set Y} (hs : AnalyticSet s) {f : X → Y} (hf : Continuous f) : AnalyticSet (f ⁻¹' s) :=
  by
  rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨Z, _, _, g, hg, rfl⟩
  have : IsClosed {x : X × Z | f x.1 = g x.2} := isClosed_eq hf.fst' hg.snd'
  convert this.analyticSet.image_of_continuous continuous_fst
  ext x
  simp [eq_comm]

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