Theorems · Definition · general topology

PolishSpace.IsClopenable

{α : Type u_1} → [t : TopologicalSpace α] → Set α → Prop

A set in a topological space is clopenable if there exists a finer Polish topology for which this set is open and closed. It turns out that this notion is equivalent to being Borel-measurable, but this is nontrivial (see isClopenable_iff_measurableSet).

Defined in

Mathlib.Topology.MetricSpace.Polish

Cited by

7 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpace