---

Step * 1 of Lemma grp_op_preserves_le


1. ∀[g:OCMon]. ∀[z:|g|].  monot(|g|;x,y.↑(x ≤b y);λw.(z * w))
⊢ ∀[g:OCMon]. ∀[x,y,z:|g|].  (x * y) ≤ (x * z) supposing y ≤ z
BY
{ (Eval ``monot`` 1 ⋅ THEN Fold `grp_leq` 1   ⋅) }

1
1. ∀[g:OCMon]. ∀[z:|g|].  ∀x,y:|g|.  ((x ≤ y) ⇒ ((z * x) ≤ (z * y)))
⊢ ∀[g:OCMon]. ∀[x,y,z:|g|].  (x * y) ≤ (x * z) supposing y ≤ z

---

Latex:

---

Latex:

1.  \mforall{}[g:OCMon].  \mforall{}[z:|g|].    monot(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}w.(z  *  w))
\mvdash{}  \mforall{}[g:OCMon].  \mforall{}[x,y,z:|g|].    (x  *  y)  \mleq{}  (x  *  z)  supposing  y  \mleq{}  z


By

---

Latex:
(Eval  ``monot``  1  \mcdot{}  THEN  Fold  `grp\_leq`  1      \mcdot{})

---

Home Index