Theorems · Definition · order theory

IsCompactlyGenerated.BooleanGenerators.recOn

{α : Type u_1} →
  [inst : CompleteLattice α] →
    {S : Set α} →
      {motive : IsCompactlyGenerated.BooleanGenerators S → Sort u} →
        (t : IsCompactlyGenerated.BooleanGenerators S) →
          ((isAtom : ∀ I ∈ S, IsAtom I) →
              (finitelyAtomistic :
                  ∀ (s : Finset α) (a : α), ↑s ⊆ S → IsCompactElement a → a ≤ s.sup id → ∃ t ⊆ s, a = t.sup id) →
                motive ⋯) →
            motive t

Defined in

Mathlib.Order.BooleanGenerators

Cited by

0 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLattice