In my opinion, current area of circle proof shouldn't be moved to the main part yet, but not only because it's a "fruit of the poison tree", but also since of the ongoing formalization of measure theory in set.mm. As far as I understand, Glauco Siliprandi's mathbox already contains the formalization of the n-dimensional Lebesgue measure on RR ^m X, as well as theorems about volumes of n-dimensional cubes, etc. It seems that this is more or less enough to reduce the computation of the area to essentially the same integral which was computed in areacirc.
As for the other results, like Heine-Cantor theorem and especially Brouwer fixed point theorem for the unit cube, they certainly deserve being moved to the main part. Since there are no sections in your mathbox, these theorems do not appear in the table of contents and remain a bit obscure. Half-angle theorems probably can be moved to the section "The exponential, sine and cosine functions" of "Elementary trigonometry"; there's already a group of statements about addition/subtraction formulae for trigonometric functions. среда, 28 июля 2021 г. в 19:23:11 UTC+7, [email protected]: > I've heard others say some of my theorems should be moved to the main > body, in particular the area of a circle. As I have it currently, the area > of a circle is based on a strange variant of the Fundamental Theorem of > Calculus, based on a notion of the integral that is, frankly, not the > integral at all, since it's based on a measure that's a submeasure. It > could, of course, very easily be rewritten to rely on the principle of > countable choice. Moreover, some of my theorems dodging this principle are > strictly as good (bddibl and cniccibl) or better (itg2add), even if they > are fruit of a poison tree. > > And then there are less controversial ones, like the Poincare-Miranda > theorem, or the Heine-Cantor theorem, or pi being strictly greater than 3. > And there are those I'm not sure the main body has a place for, like the > half-angle theorem. > -- 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/d9229d97-a4e8-4b20-84ce-eb1fab4aea08n%40googlegroups.com.
