Theorems · Definition · order theory

CompletelyDistribLattice.casesOn

{α : Type u} →
  {motive : CompletelyDistribLattice α → Sort u_1} →
    (t : CompletelyDistribLattice α) →
      ([toCompleteLattice : CompleteLattice α] →
          [toHImp : HImp α] →
            (le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) →
              [toCompl : Compl α] →
                (himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ) →
                  [toSDiff : SDiff α] →
                    (sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) →
                      [toHNot : HNot α] →
                        (top_sdiff : ∀ (a : α), ⊤ \ a = ￢a) →
                          (iInf_iSup_eq :
                              ∀ {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α),
                                ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)) →
                            motive
                              { toCompleteLattice := toCompleteLattice, toHImp := toHImp, le_himp_iff := le_himp_iff,
                                toCompl := toCompl, himp_bot := himp_bot, toSDiff := toSDiff,
                                sdiff_le_iff := sdiff_le_iff, toHNot := toHNot, top_sdiff := top_sdiff,
                                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