Documentation

Mathlib.Order.BooleanGenerators

Generators for boolean algebras #

In this file, we provide an alternative constructor for boolean algebras.

A set of boolean generators in a compactly generated complete lattice is a subset S such that

Main declarations #

An alternative constructor for boolean algebras.

A set of boolean generators in a compactly generated complete lattice is a subset S such that

  • the elements of S are all atoms, and
  • the set S satisfies an atomicity condition: any compact element below the supremum of a finite subset s of generators is equal to the supremum of a subset of s.

If the supremum of S is the whole lattice, then the lattice is a boolean algebra (see IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top).

  • isAtom : IS, IsAtom I

    The elements in a collection of boolean generators are all atoms.

  • finitelyAtomistic : ∀ (s : Finset α) (a : α), s SCompleteLattice.IsCompactElement aa s.sup idts, a = t.sup id

    The elements in a collection of boolean generators satisfy an atomicity condition: any compact element below the supremum of a finite subset s of generators is equal to the supremum of a subset of s.

Instances For

    The elements in a collection of boolean generators are all atoms.

    theorem IsCompactlyGenerated.BooleanGenerators.finitelyAtomistic {α : Type u_1} [CompleteLattice α] {S : Set α} (self : IsCompactlyGenerated.BooleanGenerators S) (s : Finset α) (a : α) :
    s SCompleteLattice.IsCompactElement aa s.sup idts, a = t.sup id

    The elements in a collection of boolean generators satisfy an atomicity condition: any compact element below the supremum of a finite subset s of generators is equal to the supremum of a subset of s.

    theorem IsCompactlyGenerated.BooleanGenerators.sSup_inter {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : IsCompactlyGenerated.BooleanGenerators S) {T₁ : Set α} {T₂ : Set α} (hT₁ : T₁ S) (hT₂ : T₂ S) :
    sSup (T₁ T₂) = sSup T₁ sSup T₂

    A lattice generated by boolean generators is a distributive lattice.

    Equations
    Instances For

      A compactly generated complete lattice generated by boolean generators is a boolean algebra.

      Equations
      Instances For