Theorems · Definition

CompleteDistribLattice.copy

{α : Type u} →
  (c : CompleteDistribLattice α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (bot : α) →
              bot = ⊥ →
                (sup : α → α → α) →
                  sup = max →
                    (inf : α → α → α) →
                      inf = min →
                        (sdiff : α → α → α) →
                          sdiff = SDiff.sdiff →
                            (hnot : α → α) →
                              hnot = HNot.hnot →
                                (himp : α → α → α) →
                                  himp = HImp.himp →
                                    (compl : α → α) →
                                      compl = Compl.compl →
                                        (sSup : Set α → α) →
                                          sSup = SupSet.sSup →
                                            (sInf : Set α → α) → sInf = InfSet.sInf → CompleteDistribLattice α

A function to create a provable equal copy of a complete distributive lattice with possibly different definitional equalities.

Defined in

Mathlib.Order.Copy

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound