---

Step * 2 of Lemma order-preserving-map-lattice-lemma


1. l1 : Lattice
2. l2 : Lattice
3. f : Point(l1) ⟶ Point(l2)
4. ∀x,y:Point(l1).  (x ≤ y ⇒ f x ≤ f y)
5. ∀a,b:Point(l1).  f a ∧ b ≤ f a ∧ f b
6. a : Point(l1)@i
7. b : Point(l1)@i
⊢ f a ∨ f b ≤ f a ∨ b
BY
{ ((InstLemma `lattice-join-is-lub` [⌜l1⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN (InstLemma `lattice-join-is-lub` [⌜l2⌝;⌜f a⌝;⌜f b⌝]⋅ THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  l1  :  Lattice
2.  l2  :  Lattice
3.  f  :  Point(l1)  {}\mrightarrow{}  Point(l2)
4.  \mforall{}x,y:Point(l1).    (x  \mleq{}  y  {}\mRightarrow{}  f  x  \mleq{}  f  y)
5.  \mforall{}a,b:Point(l1).    f  a  \mwedge{}  b  \mleq{}  f  a  \mwedge{}  f  b
6.  a  :  Point(l1)@i
7.  b  :  Point(l1)@i
\mvdash{}  f  a  \mvee{}  f  b  \mleq{}  f  a  \mvee{}  b


By

---

Latex:
((InstLemma  `lattice-join-is-lub`  [\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `lattice-join-is-lub`  [\mkleeneopen{}l2\mkleeneclose{};\mkleeneopen{}f  a\mkleeneclose{};\mkleeneopen{}f  b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index