Re: [isabelle] Trying to fit HOL to traditional math verbiage

On 08/11/11 05:00, James Frank wrote:
> To prove that f is a function, you have to show that for every element
> in the domain, there exists an element in the codomain that it's mapped
> to. But the best you might can do is show that it maps to an element in
> some interval.

What?  Why?

> So someone, somewhere back  in history, conveniently
> decided to loosen up the definition of function to allow that.

To allow what?  I'm not convinced that anyone deliberately decided that
the definition of functions shouldn't correspond with how mathematicians
actually think about them.  I think it's just a long-standing imprecision.

> Otherwise, a tighter definition of function becomes a big show stopper.

Why?  Can you give an example?

> --James


Attachment: signature.asc
Description: OpenPGP digital signature

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