Step
*
of Lemma
grp_lt_is_sp_of_leq_a
∀[g:OMon]. ∀[a,b:|g|]. uiff(a < b;(a ≤ b) ∧ (¬(b ≤ a)))
BY
{ ProveSpecializedLemma `set_lt_is_sp_of_leq_a` 1 [parm{i};g↓oset] ((AbReduceC ANDTHENC FoldsC ``grp_lt grp_leq``)) }
Latex:
Latex:
\mforall{}[g:OMon]. \mforall{}[a,b:|g|]. uiff(a < b;(a \mleq{} b) \mwedge{} (\mneg{}(b \mleq{} a)))
By
Latex:
ProveSpecializedLemma `set\_lt\_is\_sp\_of\_leq\_a` 1 [parm\{i\};g\mdownarrow{}oset
] ((AbReduceC ANDTHENC FoldsC ``grp\_lt grp\_leq``))
Home
Index