Add tau to Jim Kingdon's mathbox
Add tau to Jim Kingdon's mathbox

This is the ratio of a circle's circumference to its radius.

Use italic and the customary color for variables for (propositional
logic) variable ta , and non-italic and the customer color for
constants for constant tau . This is similar to the difference
between V and _V .

Show that tau equals 2 x. pi

We have most of the pieces in coseq1 , several infimum theorems,
theorems about RR+ , etc.

Here's what we add:

pirp - pi is a positive real
taupilem1 , taupilem2 , taupilem3 - lemmas for the proof of taupi
taupilemrplb - a set of positive reals, considered as a subset
  of the reals, has a lower bound
taupi - tau is two times pi

metamath/set.mm,metamath/set.mm,metamath/set.mm