Theorems · Definition · order theory

CompleteAtomicBooleanAlgebra.casesOn

{α : Type u} →
  {motive : CompleteAtomicBooleanAlgebra α → Sort u_1} →
    (t : CompleteAtomicBooleanAlgebra α) →
      ([toCompleteBooleanAlgebra : CompleteBooleanAlgebra α] →
          (iInf_iSup_eq :
              ∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)) →
            motive { toCompleteBooleanAlgebra := toCompleteBooleanAlgebra, iInf_iSup_eq := iInf_iSup_eq }) →
        motive t

Defined in

Mathlib.Order.CompleteBooleanAlgebra

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms