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