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

Tim
<><

Attachment: signature.asc
Description: OpenPGP digital signature



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