Documentation

Mathlib.MeasureTheory.SetAlgebra

Algebra of sets #

In this file we define the notion of algebra of sets and give its basic properties. An algebra of sets is a family of sets containing the empty set and closed by complement and binary union. It is therefore similar to a ฯƒ-algebra, except that it is not necessarily closed by countable unions.

We also define the algebra of sets generated by a family of sets and give its basic properties, and we prove that it is countable when it is generated by a countable family. We prove that the ฯƒ-algebra generated by a family of sets ๐’œ is the same as the one generated by the algebra of sets generated by ๐’œ.

Main definitions #

Main statements #

References #

Tags #

algebra of sets, generated algebra of sets

Definition and basic properties of an algebra of sets #

structure MeasureTheory.IsSetAlgebra {ฮฑ : Type u_1} (๐’œ : Set (Set ฮฑ)) :

An algebra of sets is a family of sets containing the empty set and closed by complement and union. Consequently it is also closed by difference (see IsSetAlgebra.diff_mem) and intersection (see IsSetAlgebra.inter_mem).

Instances For
    theorem MeasureTheory.IsSetAlgebra.empty_mem {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} (self : MeasureTheory.IsSetAlgebra ๐’œ) :
    โˆ… โˆˆ ๐’œ
    theorem MeasureTheory.IsSetAlgebra.compl_mem {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} (self : MeasureTheory.IsSetAlgebra ๐’œ) โฆƒs : Set ฮฑโฆ„ :
    s โˆˆ ๐’œ โ†’ sแถœ โˆˆ ๐’œ
    theorem MeasureTheory.IsSetAlgebra.union_mem {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} (self : MeasureTheory.IsSetAlgebra ๐’œ) โฆƒs : Set ฮฑโฆ„ โฆƒt : Set ฮฑโฆ„ :
    s โˆˆ ๐’œ โ†’ t โˆˆ ๐’œ โ†’ s โˆช t โˆˆ ๐’œ
    theorem MeasureTheory.IsSetAlgebra.univ_mem {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} (h๐’œ : MeasureTheory.IsSetAlgebra ๐’œ) :
    Set.univ โˆˆ ๐’œ

    An algebra of sets contains the whole set.

    theorem MeasureTheory.IsSetAlgebra.inter_mem {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} {s : Set ฮฑ} {t : Set ฮฑ} (h๐’œ : MeasureTheory.IsSetAlgebra ๐’œ) (s_mem : s โˆˆ ๐’œ) (t_mem : t โˆˆ ๐’œ) :
    s โˆฉ t โˆˆ ๐’œ

    An algebra of sets is closed by intersection.

    theorem MeasureTheory.IsSetAlgebra.diff_mem {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} {s : Set ฮฑ} {t : Set ฮฑ} (h๐’œ : MeasureTheory.IsSetAlgebra ๐’œ) (s_mem : s โˆˆ ๐’œ) (t_mem : t โˆˆ ๐’œ) :
    s \ t โˆˆ ๐’œ

    An algebra of sets is closed by difference.

    theorem MeasureTheory.IsSetAlgebra.isSetRing {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} (h๐’œ : MeasureTheory.IsSetAlgebra ๐’œ) :

    An algebra of sets is a ring of sets.

    theorem MeasureTheory.IsSetAlgebra.biUnion_mem {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} {ฮน : Type u_2} (h๐’œ : MeasureTheory.IsSetAlgebra ๐’œ) {s : ฮน โ†’ Set ฮฑ} (S : Finset ฮน) (hs : โˆ€ i โˆˆ S, s i โˆˆ ๐’œ) :
    โ‹ƒ i โˆˆ S, s i โˆˆ ๐’œ

    An algebra of sets is closed by finite unions.

    theorem MeasureTheory.IsSetAlgebra.biInter_mem {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} {ฮน : Type u_2} (h๐’œ : MeasureTheory.IsSetAlgebra ๐’œ) {s : ฮน โ†’ Set ฮฑ} (S : Finset ฮน) (hs : โˆ€ i โˆˆ S, s i โˆˆ ๐’œ) :
    โ‹‚ i โˆˆ S, s i โˆˆ ๐’œ

    An algebra of sets is closed by finite intersections.

    Definition and properties of the algebra of sets generated by some family #

    inductive MeasureTheory.generateSetAlgebra {ฮฑ : Type u_1} (๐’œ : Set (Set ฮฑ)) :
    Set (Set ฮฑ)

    generateSetAlgebra ๐’œ is the smallest algebra of sets containing ๐’œ.

    Instances For

      The algebra of sets generated by a family of sets is an algebra of sets.

      theorem MeasureTheory.self_subset_generateSetAlgebra {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} :

      The algebra of sets generated by ๐’œ contains ๐’œ.

      @[simp]

      The measurable space generated by a family of sets ๐’œ is the same as the one generated by the algebra of sets generated by ๐’œ.

      theorem MeasureTheory.generateSetAlgebra_mono {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} {โ„ฌ : Set (Set ฮฑ)} (h : ๐’œ โŠ† โ„ฌ) :

      If a family of sets ๐’œ is contained in โ„ฌ, then the algebra of sets generated by ๐’œ is contained in the one generated by โ„ฌ.

      theorem MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} {โ„ฌ : Set (Set ฮฑ)} (h : ๐’œ โŠ† โ„ฌ) (hโ„ฌ : MeasureTheory.IsSetAlgebra โ„ฌ) :

      If a family of sets ๐’œ is contained in an algebra of sets โ„ฌ, then so is the algebra of sets generated by ๐’œ.

      theorem MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset_self {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} (h๐’œ : MeasureTheory.IsSetAlgebra ๐’œ) :

      If ๐’œ is an algebra of sets, then it contains the algebra generated by itself.

      theorem MeasureTheory.IsSetAlgebra.generateSetAlgebra_eq {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} (h๐’œ : MeasureTheory.IsSetAlgebra ๐’œ) :

      If ๐’œ is an algebra of sets, then it is equal to the algebra generated by itself.

      theorem MeasureTheory.mem_generateSetAlgebra_elim {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} {s : Set ฮฑ} (s_mem : s โˆˆ MeasureTheory.generateSetAlgebra ๐’œ) :
      โˆƒ (A : Set (Set (Set ฮฑ))), A.Finite โˆง (โˆ€ a โˆˆ A, a.Finite) โˆง (โˆ€ a โˆˆ A, โˆ€ t โˆˆ a, t โˆˆ ๐’œ โˆจ tแถœ โˆˆ ๐’œ) โˆง s = โ‹ƒ a โˆˆ A, โ‹‚ t โˆˆ a, t

      If a set belongs to the algebra of sets generated by ๐’œ then it can be written as a finite union of finite intersections of sets which are in ๐’œ or have their complement in ๐’œ.

      theorem MeasureTheory.countable_generateSetAlgebra {ฮฑ : Type u_1} {๐’œ : Set (Set ฮฑ)} (h : ๐’œ.Countable) :
      (MeasureTheory.generateSetAlgebra ๐’œ).Countable

      If a family of sets is countable then so is the algebra of sets generated by it.