*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Thu, 10 Nov 2011 11:50:28 +1300*In-reply-to*: <4EB800A2.2020200@gmx.com>*References*: <4EB2E13B.507@gmx.com> <CAMej=25im4emE5QFAxDduhCbEkfLuu9r2YDi4P0hd2w=-9_qMg@mail.gmail.com> <4EB42510.7020408@gmx.com> <CAMej=248dGYvfRCFOK+L0JtyvmDeF-eEoA-f9a-XEro6+yMSew@mail.gmail.com> <4EB5709A.3090203@gmx.com> <CAFP4q16dyEd=_SeC28GDN6kFkwTUyJvO-+_htuwXgNjsu8B43w@mail.gmail.com> <4EB654A4.6010500@netspeed.com.au> <4EB70322.3010507@gmail.com> <4EB800A2.2020200@gmx.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.23) Gecko/20110921 Thunderbird/3.1.15

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**

**Follow-Ups**:**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**References**:**[isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Josef Urban

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Jeremy Dawson

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Tim (McKenzie) Makarios

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

- Previous by Date: Re: [isabelle] primrec
- Next by Date: [isabelle] No Code Equation for LIMSEQ
- Previous by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Cl-isabelle-users November 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list