Step
*
of Lemma
grp_op_preserves_le
∀[g:OCMon]. ∀[x,y,z:|g|].  (x * y) ≤ (x * z) supposing y ≤ z
BY
{ AssertLemma `ocmon_6` [] }
1
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
Latex:
Latex:
\mforall{}[g:OCMon].  \mforall{}[x,y,z:|g|].    (x  *  y)  \mleq{}  (x  *  z)  supposing  y  \mleq{}  z
By
Latex:
AssertLemma  `ocmon\_6`  []
Home
Index