Mathlib Map

Theorems · Inductive type · measure theory

MeasureTheory.generateSetAlgebra

{α : Type u_2} → Set (Set α) → Set (Set α)

generateSetAlgebra 𝒜 is the smallest algebra of sets containing 𝒜.

Defined in
Mathlib.MeasureTheory.SetAlgebra
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.

MeasureTheory.self_subset_generateSetAlgebra · cited by 4MeasureTheory.self_subset…MeasureTheory.isSetAlgebra_generateSetAlgebra · cited by 2MeasureTheory.isSetAlgebr…MeasureTheory.mem_generateSetAlgebra_elim · cited by 1MeasureTheory.mem_generat…MeasureTheory.generateSetAlgebra_mono · cited by 1MeasureTheory.generateSet…MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset · cited by 1IsSetAlgebra.generateSetA…MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset_self · cited by 1IsSetAlgebra.generateSetA…MeasureTheory.countable_generateSetAlgebra · cited by 1MeasureTheory.countable_g…MeasureTheory.generateSetAlgebra.below · cited by 1generateSetAlgebra.belowMeasureTheory.generateSetAlgebra.recOn · cited by 0generateSetAlgebra.recOnMeasureTheory.isSeparable_of_sigmaFinite · cited by 0MeasureTheory.isSeparable…MeasureTheory.generateFrom_generateSetAlgebra_eq · cited by 0MeasureTheory.generateFro…MeasureTheory.IsSetAlgebra.generateSetAlgebra_eq · cited by 0IsSetAlgebra.generateSetA…MeasureTheory.generateSetAlgebra.below.casesOn · cited by 0below.casesOnMeasureTheory.generateSetAlgebra.brecOn · cited by 0generateSetAlgebra.brecOnMeasureTheory.generateSetAlgebra.casesOn · cited by 0generateSetAlgebra.casesOnSet · cited by 53352SetMeasureTheory.generateSetAlge…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 by15

Results whose statement or proof uses this declaration.