---

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

∀[l1,l2:Lattice]. ∀[f:Point(l1) ⟶ Point(l2)].
  (∀a,b:Point(l1).  f a ∧ b ≤ f a ∧ f b) ∧ (∀a,b:Point(l1).  f a ∨ f b ≤ f a ∨ b) 
  supposing ∀x,y:Point(l1).  (x ≤ y ⇒ f x ≤ f y)
BY
{ Auto }

1
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 : Point(l1)@i
6. b : Point(l1)@i
⊢ f a ∧ b ≤ f a ∧ f b

2
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

---

Latex:

---

Latex:
\mforall{}[l1,l2:Lattice].  \mforall{}[f:Point(l1)  {}\mrightarrow{}  Point(l2)].
    (\mforall{}a,b:Point(l1).    f  a  \mwedge{}  b  \mleq{}  f  a  \mwedge{}  f  b)  \mwedge{}  (\mforall{}a,b:Point(l1).    f  a  \mvee{}  f  b  \mleq{}  f  a  \mvee{}  b) 
    supposing  \mforall{}x,y:Point(l1).    (x  \mleq{}  y  {}\mRightarrow{}  f  x  \mleq{}  f  y)


By

---

Latex:
Auto

---

Home Index