polishSpace — Mathlib

English

An open subset of a Polish space is itself Polish when endowed with the subspace topology.

Русский

Открытое подмножество полиспейса сохраняет свойство полишпространства под подпространством.

LaTeX

$$$\text{PolishSpace}(s)$$$

Lean4

/-- An open subset of a Polish space is also Polish. -/
theorem _root_.IsOpen.polishSpace {α : Type*} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsOpen s) :
    PolishSpace s := by
  letI := upgradeIsCompletelyMetrizable α
  lift s to Opens α using hs
  exact inferInstanceAs (PolishSpace s.CompleteCopy)

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