On Fri, 04 Oct 2019 11:24:43 -0700, Jim Kingdon <[email protected]> wrote: > Oh and I suppose I should immodestly mention the addition of > http://us2.metamath.org/mpeuni/taupi.html . But that's just me trying to keep > up my https://tauday.com creds, everyone will make up their own mind about > that one :-).
I see the advantages of tau, but I think I'll avoid claiming that as a key event :-). > On October 4, 2019 11:20:21 AM PDT, Jim Kingdon <[email protected]> wrote: > >The introduction of http://us2.metamath.org/mpeuni/df-c.html > >The introduction of http://us2.metamath.org/mpeuni/df-pi.html Those are excellent examples. df-c has a useful date. According to set.mm, df-c was contributed by NM on 22-Feb-1996 as df-c $a |- CC = ( R. X. R. ) $. That is consistent with the git repo; the first instance I can find is in commit 85655124fa08f87bb77112eb4035b48feb12c723 (stable release, archive name set.mm.1998-03-16-from-vax). df-pi is trickier to date. Paul Chapman created a definition 23-Jan-2008, but a previous and different definition of df-pi was created (presumably by Norman Megill) between 2004-09-27 and 2007-04-29. Details below. Suggestions on how to date the *first* instance of df-pi are welcome. --- David A. Wheeler ============= DETAILS ==================== Here's what set.mm currently says about df-pi: $( Define pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of pi in [Gleason] p. 311. (We use the inverse of less-than, " ` ``' < ` ", to turn supremum into infimum; currently we don't have infimum defined separately.) (Contributed by Paul Chapman, 23-Jan-2008.) $) df-pi $a |- _pi = sup ( ( RR+ i^i ( `' sin " { 0 } ) ) , RR , `' < ) $. However, the first commit with *any* df-pi in the git repo is commit ba18c14ef9713308a7efe1dfbc8049975f52f56a (stable release, archive name set.mm.2007-04-29-grothprim) which says: $( Define pi = 3.14159..., which is the smallest positive number whose sine is zero. (Note that the argument " ` ``' < ` " turns supremum into infimum; currently we don't have infimum defined separately.) $) df-pi $a |- pi = sup ( { x e. RR | ( 0 < x /\ ( sin ` x ) = 0 ) } , RR , `' < ) $. $} The previous commit c55adffeaab4685ce49f662c301a4b518b9438e6 (stable release, archive name set.mm.2004-09-27-card) does *not* have df-pi. -- 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/E1iGVhz-0007gY-NJ%40rmmprod07.runbox.
