analyticSet — Mathlib

English

A closed set in a Polish space is analytic.

Русский

Замкнутое множество в полишпространстве аналитично.

LaTeX

$$$[PolishSpace α] \; IsClosed(s) \Rightarrow AnalyticSet(s).$$$

Lean4

theorem _root_.IsClosed.analyticSet [PolishSpace α] {s : Set α} (hs : IsClosed s) : AnalyticSet s :=
  by
  haveI : PolishSpace s := hs.polishSpace
  rw [← @Subtype.range_val α s]
  exact analyticSet_range_of_polishSpace continuous_subtype_val

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