Theorems · Definition · order theory

BooleanAlgebra.casesOn

{α : Type u} →
  {motive : BooleanAlgebra α → Sort u_1} →
    (t : BooleanAlgebra α) →
      ([toDistribLattice : DistribLattice α] →
          [toCompl : Compl α] →
            [toSDiff : SDiff α] →
              [toHImp : HImp α] →
                [toTop : Top α] →
                  [toBot : Bot α] →
                    (inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥) →
                      (top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ) →
                        (le_top : ∀ (a : α), a ≤ ⊤) →
                          (bot_le : ∀ (a : α), ⊥ ≤ a) →
                            (sdiff_eq : ∀ (x y : α), x \ y = x ⊓ yᶜ) →
                              (himp_eq : ∀ (x y : α), x ⇨ y = y ⊔ xᶜ) →
                                motive
                                  { toDistribLattice := toDistribLattice, toCompl := toCompl, toSDiff := toSDiff,
                                    toHImp := toHImp, toTop := toTop, toBot := toBot,
                                    inf_compl_le_bot := inf_compl_le_bot, top_le_sup_compl := top_le_sup_compl,
                                    le_top := le_top, bot_le := bot_le, sdiff_eq := sdiff_eq, himp_eq := himp_eq }) →
        motive t

Defined in

Mathlib.Order.BooleanAlgebra.Defs

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms