Theorems · Theorem · measure theory

Inseparable.mem_measurableSet_iff

∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] {x y : γ},
  Inseparable x y → ∀ {s : Set γ}, MeasurableSet s → (x ∈ s ↔ y ∈ s)

If two points are topologically inseparable, then they can't be separated by a Borel measurable set.

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Cited by

1 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceMeasurableSpaceBorelSpace