---

Step * of Lemma mk-distributive-lattice_wf

∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T].
  mk-distributive-lattice(T; m; j) ∈ DistributiveLattice 
  supposing (∀[a,b:T].  (m[a;b] = m[b;a] ∈ T))
  ∧ (∀[a,b:T].  (j[a;b] = j[b;a] ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;m[b;c]] = m[m[a;b];c] ∈ T))
  ∧ (∀[a,b,c:T].  (j[a;j[b;c]] = j[j[a;b];c] ∈ T))
  ∧ (∀[a,b:T].  (j[a;m[a;b]] = a ∈ T))
  ∧ (∀[a,b:T].  (m[a;j[a;b]] = a ∈ T))
  ∧ (∀[a,b,c:T].  (m[a;j[b;c]] = j[m[a;b];m[a;c]] ∈ T))
BY
{ ((Auto THEN RepUR ``mk-distributive-lattice distributive-lattice`` 0)
   THEN MemTypeCD
   THEN Auto
   THEN (RepUR ``mk-lattice lattice-axioms`` 0 THEN RepUR ``lattice-point lattice-meet lattice-join`` 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m,j:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].
    mk-distributive-lattice(T;  m;  j)  \mmember{}  DistributiveLattice 
    supposing  (\mforall{}[a,b:T].    (m[a;b]  =  m[b;a]))
    \mwedge{}  (\mforall{}[a,b:T].    (j[a;b]  =  j[b;a]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (m[a;m[b;c]]  =  m[m[a;b];c]))
    \mwedge{}  (\mforall{}[a,b,c:T].    (j[a;j[b;c]]  =  j[j[a;b];c]))
    \mwedge{}  (\mforall{}[a,b:T].    (j[a;m[a;b]]  =  a))
    \mwedge{}  (\mforall{}[a,b:T].    (m[a;j[a;b]]  =  a))
    \mwedge{}  (\mforall{}[a,b,c:T].    (m[a;j[b;c]]  =  j[m[a;b];m[a;c]]))


By

---

Latex:
((Auto  THEN  RepUR  ``mk-distributive-lattice  distributive-lattice``  0)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (RepUR  ``mk-lattice  lattice-axioms``  0
              THEN  RepUR  ``lattice-point  lattice-meet  lattice-join``  0
              )
  THEN  Auto)

---

Home Index