Re: [isabelle] Comparing two graphs



>
> Here the order on pairs of reals is overwritten:
>  (x :: real, y :: real) < (a, b) <-> x < a /\ y < b
>
> and for the function you have:
>
>   f < g <-> ALL x. f x < g x
>
> If you don't want to import Multivariate_Analysis why not just comparing
>
>   (snd o f) < (snd o g)
>
> this compares the second components of f and g.

Thanks. If my notion of < compares the snd of each pair, should I
import Multivariate_Analysis and then overwrite < or should I just
define my own < without Multivariate_Analysis?

Thanks

John
>
>
>
>
>> I see that two pairs can't be compared with each other, but in my
>> situation I'd like to say that one is less than another if its y
>> (second) value is lower. As for comparing two such graphs, then it's a
>> matter of summing up all of the y (second) values and see which is
>> smaller.
>>
>> Does anyone know of a good way of achieving this kind of comparison?
>>
>> Thanks a lot for your time.
>>
>> John
>>
>
>
>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.