---

Step * of Lemma lattice-axioms-iff-order

∀l:LatticeStructure
  (∃R:Point(l) ⟶ Point(l) ⟶ ℙ
    (((∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b))
    ∧ (∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)))
    ∧ Order(Point(l);x,y.R[x;y]))
  ⇐⇒ lattice-axioms(l))
BY
{ (Auto THEN Try ((BLemma `lattice-axioms-from-order` THEN Auto))) }

1
1. l : LatticeStructure@i'
2. lattice-axioms(l)@i
⊢ ∃R:Point(l) ⟶ Point(l) ⟶ ℙ
   (((∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b))
   ∧ (∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)))
   ∧ Order(Point(l);x,y.R[x;y]))

---

Latex:

---

Latex:
\mforall{}l:LatticeStructure
    (\mexists{}R:Point(l)  {}\mrightarrow{}  Point(l)  {}\mrightarrow{}  \mBbbP{}
        (((\mforall{}[a,b:Point(l)].    least-upper-bound(Point(l);x,y.R[x;y];a;b;a  \mvee{}  b))
        \mwedge{}  (\mforall{}[a,b:Point(l)].    greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a  \mwedge{}  b)))
        \mwedge{}  Order(Point(l);x,y.R[x;y]))
    \mLeftarrow{}{}\mRightarrow{}  lattice-axioms(l))


By

---

Latex:
(Auto  THEN  Try  ((BLemma  `lattice-axioms-from-order`  THEN  Auto)))

---

Home Index