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

@[deprecated MeasureTheory.IsSetAlgebra.sdiff_mem (since := "2026-06-03")]

theorem MeasureTheory.IsSetAlgebra.diff_mem {α : Type u_1} {𝒜 : Set (Set α)} {s t : Set α} (h𝒜 : IsSetAlgebra 𝒜) (s_mem : s ∈ 𝒜) (t_mem : t ∈ 𝒜) : s \ t ∈ 𝒜

Alias of MeasureTheory.IsSetAlgebra.sdiff_mem.

---

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

def MeasureTheory.generateSetAlgebra {α : Type u_2} (𝒜 : Set (Set α)) : Set (Set α)

generateSetAlgebra 𝒜 is the smallest algebra of sets containing 𝒜.

Equations

• MeasureTheory.generateSetAlgebra 𝒜 = {s : Set α | MeasureTheory.GenerateSetAlgebra✝ 𝒜 s}

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

theorem MeasureTheory.generateSetAlgebra_induction {α : Type u_1} {𝒜 : Set (Set α)} {s : Set α} {motive : (s : Set α) → s ∈ generateSetAlgebra 𝒜 → Prop} (base : ∀ (u : Set α) (hu : u ∈ 𝒜), motive u ⋯) (empty : motive ∅ ⋯) (compl : ∀ (u : Set α) (hu : u ∈ generateSetAlgebra 𝒜), motive u hu → motive uᶜ ⋯) (union : ∀ (u v : Set α) (hu : u ∈ generateSetAlgebra 𝒜) (hv : v ∈ generateSetAlgebra 𝒜), motive u hu → motive v hv → motive (u ∪ v) ⋯) (hs : s ∈ generateSetAlgebra 𝒜) : motive s hs

An induction principle for membership of generateSetAlgebra 𝒜. If motive holds of all elements of 𝒜 and of ∅, and is preserved under complement and binary union, then it holds of all elements of generateSetAlgebra 𝒜.

theorem MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset {α : Type u_1} {𝒜 ℬ : Set (Set α)} (h : 𝒜 ⊆ ℬ) (hℬ : IsSetAlgebra ℬ) : generateSetAlgebra 𝒜 ⊆ ℬ

generateSetAlgebra 𝒜 is the smallest algebra of sets containing 𝒜: if a family of sets 𝒜 is contained in an algebra of sets ℬ, then so is the algebra of sets generated by 𝒜.

@[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_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.