Theorems · Definition · order theory

BiheytingAlgebra.casesOn

{α : Type u_4} →
  {motive : BiheytingAlgebra α → Sort u} →
    (t : BiheytingAlgebra α) →
      ([toHeytingAlgebra : HeytingAlgebra α] →
          [toSDiff : SDiff α] →
            (sdiff_le_iff : ∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) →
              [toHNot : HNot α] →
                (top_sdiff : ∀ (a : α), ⊤ \ a = ￢a) →
                  motive
                    { toHeytingAlgebra := toHeytingAlgebra, toSDiff := toSDiff, sdiff_le_iff := sdiff_le_iff,
                      toHNot := toHNot, top_sdiff := top_sdiff }) →
        motive t

Defined in

Mathlib.Order.Heyting.Basic

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms