Theorems · Definition

GeneralizedHeytingAlgebra.copy

{α : Type u} →
  (c : GeneralizedHeytingAlgebra α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (sup : α → α → α) →
              sup = max →
                (inf : α → α → α) → inf = min → (himp : α → α → α) → himp = HImp.himp → GeneralizedHeytingAlgebra α

A function to create a provable equal copy of a generalised heyting algebra with possibly different definitional equalities.

Defined in

Mathlib.Order.Copy

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext