Theorems · Definition · order theory

Order.Frame.recOn

{α : Type u_1} →
  {motive : Order.Frame α → Sort u} →
    (t : Order.Frame α) →
      ([toCompleteLattice : CompleteLattice α] →
          [toHImp : HImp α] →
            (le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) →
              [toCompl : Compl α] →
                (himp_bot : ∀ (a : α), a ⇨ ⊥ = aᶜ) →
                  motive
                    { toCompleteLattice := toCompleteLattice, toHImp := toHImp, le_himp_iff := le_himp_iff,
                      toCompl := toCompl, himp_bot := himp_bot }) →
        motive t

Defined in

Mathlib.Order.CompleteBooleanAlgebra

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms