---

Step * 1 1 of Lemma lattice-axioms-iff-order


1. l : LatticeStructure@i'
2. lattice-axioms(l)@i
3. λ2a b.a ≤ b ∈ Point(l) ⟶ Point(l) ⟶ ℙ
⊢ ∃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]))
BY
{ Assert ⌜((∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.λ2a b.a ≤ b[x;y];a;b;a ∨ b))
          ∧ (∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.λ2a b.a ≤ b[x;y];a;b;a ∧ b)))
          ∧ Order(Point(l);x,y.λ2a b.a ≤ b[x;y])⌝⋅ }

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

2
1. l : LatticeStructure@i'
2. lattice-axioms(l)@i
3. λ2a b.a ≤ b ∈ Point(l) ⟶ Point(l) ⟶ ℙ
4. ((∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.λ2a b.a ≤ b[x;y];a;b;a ∨ b))
∧ (∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.λ2a b.a ≤ b[x;y];a;b;a ∧ b)))
∧ Order(Point(l);x,y.λ2a b.a ≤ b[x;y])
⊢ ∃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:

1.  l  :  LatticeStructure@i'
2.  lattice-axioms(l)@i
3.  \mlambda{}\msubtwo{}a  b.a  \mleq{}  b  \mmember{}  Point(l)  {}\mrightarrow{}  Point(l)  {}\mrightarrow{}  \mBbbP{}
\mvdash{}  \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]))


By

---

Latex:
Assert  \mkleeneopen{}((\mforall{}[a,b:Point(l)].    least-upper-bound(Point(l);x,y.\mlambda{}\msubtwo{}a  b.a  \mleq{}  b[x;y];a;b;a  \mvee{}  b))
                \mwedge{}  (\mforall{}[a,b:Point(l)].    greatest-lower-bound(Point(l);x,y.\mlambda{}\msubtwo{}a  b.a  \mleq{}  b[x;y];a;b;a  \mwedge{}  b)))
                \mwedge{}  Order(Point(l);x,y.\mlambda{}\msubtwo{}a  b.a  \mleq{}  b[x;y])\mkleeneclose{}\mcdot{}

---

Home Index