Mathlib Map

Theorems · Inductive type · measure theory

MeasurableSpace.GenerateMeasurable

{α : Type u_1} → Set (Set α) → Set α → Prop

The smallest σ-algebra containing a collection s of basic sets

Defined in
Mathlib.MeasureTheory.MeasurableSpace.Defs
Cited by
11 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasurableSpace.generateFrom · cited by 172MeasurableSpace.generateF…MeasurableSpace.generateFrom_le · cited by 49MeasurableSpace.generateF…MeasurableSpace.generateFrom_induction · cited by 7MeasurableSpace.generateF…MeasurableSpace.cardinal_generateMeasurable_le · cited by 2MeasurableSpace.cardinal_…MeasurableSpace.generateMeasurableRec_subset · cited by 2MeasurableSpace.generateM…MeasurableSpace.generateMeasurable_eq_rec · cited by 2MeasurableSpace.generateM…MeasurableSpace.cardinal_generateMeasurable_le_continuum · cited by 1MeasurableSpace.cardinal_…MeasurableSpace.measurableSet_iSup · cited by 1MeasurableSpace.measurabl…MeasurableSpace.GenerateMeasurable.below · cited by 1GenerateMeasurable.belowMeasurableSpace.GenerateMeasurable.recOn · cited by 1GenerateMeasurable.recOnMeasurableSpace.GenerateMeasurable.brecOn · cited by 0GenerateMeasurable.brecOnMeasurableSpace.GenerateMeasurable.below.casesOn · cited by 0below.casesOnMeasurableSpace.measurableSet_sSup · cited by 0MeasurableSpace.measurabl…MeasurableSpace.GenerateMeasurable.casesOn · cited by 0GenerateMeasurable.casesOnMeasurableSpace.measurableSet_sup · cited by 0MeasurableSpace.measurabl…Set · cited by 53352SetMeasurableSpace.GenerateMeasu…CITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352

Cited by16

Results whose statement or proof uses this declaration.