Re: [isabelle] Inequality assumption
HOL is a total logic, so all functions must be defined for all inputs of
the corresponding type. In Isabelle/HOL, division by zero is therefore
defined to yield zero, and with that, the lemma you cited holds.
Understanding the definitions of the constants involved in a statement
and how they differ from âstandardâ mathematical definitions is crucial.
On 05/07/16 17:22, Omar Jasim wrote:
I've seen this lemma in Fields theory:
"[|a â b; 0 â c|] ==> a/c â b/c"
by (force simp add: divide_strict_right_mono le_less)
here 0 â c which I think it should be 0 < c as the division cann't done for
This archive was generated by a fusion of
Pipermail (Mailman edition) and