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

• MeasureTheory.IsSetAlgebra: property of being an algebra of sets.
• MeasureTheory.generateSetAlgebra: the algebra of sets generated by a family of sets.

Main statements

• MeasureTheory.mem_generateSetAlgebra_elim: If a set s 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 𝒜.
• MeasureTheory.countable_generateSetAlgebra: If a family of sets is countable then so is the algebra of sets generated by it.

References

• https://en.wikipedia.org/wiki/Field_of_sets

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 α)) : Prop

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).

• empty_mem : ∅ ∈ 𝒜
• compl_mem ⦃s : Set α⦄ : s ∈ 𝒜 → sᶜ ∈ 𝒜
• union_mem ⦃s t : Set α⦄ : s ∈ 𝒜 → t ∈ 𝒜 → s ∪ t ∈ 𝒜

theorem MeasureTheory.IsSetAlgebra.univ_mem {α : Type u_1} {𝒜 : Set (Set α)} (h𝒜 : IsSetAlgebra 𝒜) : Set.univ ∈ 𝒜

An algebra of sets contains the whole set.

theorem MeasureTheory.IsSetAlgebra.inter_mem {α : Type u_1} {𝒜 : Set (Set α)} {s t : Set α} (h𝒜 : 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 t : Set α} (h𝒜 : 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𝒜 : IsSetAlgebra 𝒜) : IsSetRing 𝒜

An algebra of sets is a ring of sets.

theorem MeasureTheory.IsSetAlgebra.biUnion_mem {α : Type u_1} {𝒜 : Set (Set α)} {ι : Type u_2} (h𝒜 : 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𝒜 : 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_2} (𝒜 : Set (Set α)) : Set (Set α)

generateSetAlgebra 𝒜 is the smallest algebra of sets containing 𝒜.

• base {α : Type u_2} {𝒜 : Set (Set α)} (s : Set α) (s_mem : s ∈ 𝒜) : generateSetAlgebra 𝒜 s
• empty {α : Type u_2} {𝒜 : Set (Set α)} : generateSetAlgebra 𝒜 ∅
• compl {α : Type u_2} {𝒜 : Set (Set α)} (s : Set α) (hs : generateSetAlgebra 𝒜 s) : generateSetAlgebra 𝒜 sᶜ
• union {α : Type u_2} {𝒜 : Set (Set α)} (s t : Set α) (hs : generateSetAlgebra 𝒜 s) (ht : generateSetAlgebra 𝒜 t) : generateSetAlgebra 𝒜 (s ∪ t)

theorem MeasureTheory.isSetAlgebra_generateSetAlgebra {α : Type u_1} {𝒜 : Set (Set α)} : IsSetAlgebra (generateSetAlgebra 𝒜)

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 α)} : 𝒜 ⊆ generateSetAlgebra 𝒜

The algebra of sets generated by 𝒜 contains 𝒜.

@[simp]

theorem MeasureTheory.generateFrom_generateSetAlgebra_eq {α : Type u_1} {𝒜 : Set (Set α)} : MeasurableSpace.generateFrom (generateSetAlgebra 𝒜) = MeasurableSpace.generateFrom 𝒜

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 α)} (h : 𝒜 ⊆ ℬ) : generateSetAlgebra 𝒜 ⊆ generateSetAlgebra ℬ

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 α)} (h : 𝒜 ⊆ ℬ) (hℬ : IsSetAlgebra ℬ) : generateSetAlgebra 𝒜 ⊆ ℬ

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𝒜 : IsSetAlgebra 𝒜) : generateSetAlgebra 𝒜 ⊆ 𝒜

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𝒜 : IsSetAlgebra 𝒜) : generateSetAlgebra 𝒜 = 𝒜

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 ∈ 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) : (generateSetAlgebra 𝒜).Countable

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