Nothing special; I just mean that any theorem using the expression ( ( S _D F ) ` x ) should have x e. dom ( S _D F ) in the context or derivable from it. It's the same way we currently treat division by zero: if you write ( A / B ) then you should be able to prove that B is nonzero, otherwise the statement is nonsense. This is ZFC so we can't prevent such statements from being formed, and what the context is exactly is not well defined, but in practice it works well enough.
On Fri, Jan 10, 2020 at 5:40 PM Benoit <[email protected]> wrote: > On Friday, January 10, 2020 at 1:52:20 AM UTC+1, Mario Carneiro wrote: >> >> we should have guarded the application to avoid seeing it in the first >> place. >> > > How would you do that ? (I gave some ideas some time ago on this group, > but the drawbacks were deemed to outweigh the benefits.) > > Thanks, > Benoît > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/e905a8c5-271d-4f28-b9fc-7ac39688e544%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/e905a8c5-271d-4f28-b9fc-7ac39688e544%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsHqEgkD8dwHqQSayUkAx%3DKXHE0MvuxquaxbOYDkqgZCw%40mail.gmail.com.
