Theorems · Theorem · order theory

BooleanSubalgebra.closure_bot_sup_induction

∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α} {p : (g : α) → g ∈ BooleanSubalgebra.closure s → Prop},
  (∀ (x : α) (hx : x ∈ s), p x ⋯) →
    p ⊥ ⋯ →
      (∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s) (y : α) (hy : y ∈ BooleanSubalgebra.closure s),
          p x hx → p y hy → p (x ⊔ y) ⋯) →
        (∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s), p x hx → p xᶜ ⋯) →
          ∀ {x : α} (hx : x ∈ BooleanSubalgebra.closure s), p x hx

An induction principle for closure membership. If p holds for ⊥ and all elements of s, and is preserved under suprema and complement, then p holds for all elements of the closure of s.

Defined in

Mathlib.Order.BooleanSubalgebra

Cited by

2 results in Mathlib

Foundations

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

Assumes

BooleanAlgebra