Theorems · Theorem · measure theory

MeasurableSpace.measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence

∀ {α : Type u_1} {mα : MeasurableSpace α} [inst : MeasurableSpace.CountablyGenerated α] (x : α),
  measurableAtom x = MeasurableSpace.countablyGeneratedAtom α fun x_1 => x ∈ MeasurableSpace.natGeneratingSequence α x_1

The measurable atom of a point in a countably generated measurable space is given by a countablyGeneratedAtom.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace.CountablyGenerated