On Friday, October 4, 2019 at 6:05:57 PM UTC-4, David A. Wheeler wrote:
>
> 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.
>
I defined pi earlier, but I don't think there were any theorems using that
definition, so it doesn't really count. Use Paul's version.
Norm
--
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/c13d3536-61be-4a6a-8afe-d1cf37b54e73%40googlegroups.com.
