Theorems · Theorem · order theory

BooleanSubalgebra.mem_closure_iff_sup_sdiff

∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α},
  IsSublattice s → ⊥ ∈ s → ⊤ ∈ s → ∀ {a : α}, a ∈ BooleanSubalgebra.closure s ↔ ∃ t, a = t.sup fun x => ↑x.1 \ ↑x.2

Defined in

Mathlib.Order.BooleanSubalgebra

Cited by

1 results in Mathlib

Foundations

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

Assumes

BooleanAlgebra