isClopenable' — Mathlib

English

If s is measurable in a standard Borel space, there exists a Polish topology making s clopen.

Русский

Если s измеримо в стандартном пространстве Бореля, существует полиш‑топология, делающая s клип‑областью.

LaTeX

$$∃ t, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s$$

Lean4

/-- If `s` is a measurable set in a standard Borel space, there is a compatible Polish topology
making `s` clopen. -/
theorem isClopenable' {s : Set α} (hs : MeasurableSet s) :
    ∃ _ : TopologicalSpace α, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s :=
  by
  letI := upgradeStandardBorel α
  obtain ⟨t, hle, ht, s_clopen⟩ := hs.isClopenable
  refine ⟨t, ?_, ht, s_clopen⟩
  constructor
  rw [eq_borel_upgradeStandardBorel α, borel_eq_borel_of_le ht _ hle]
  infer_instance

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