On 7/3/23 15:56, Marshall Stoner wrote:
have written up everything I considered prior to the definition of the biconditional and conjugation. . . . will attach and share what I have written so far as soon as I know that I am approved for the mailing list. . . .
I'll be curious to see what you came up with and how you organize it. We have some ways of organizing material on the website, for example "How to intuitionize classical proofs" at https://us.metamath.org/ileuni/mmil.html#intuitionize , "Real and Complex Numbers" at https://us.metamath.org/mpeuni/mmcomplex.html , or "Algebraic and Topological Structures" at https://us.metamath.org/mpeuni/mmtopstr.html . All of these link to relevant theorems but add explanations or give some structure in terms of how one statement relates to another.
Making pull requests to the web site should now be possible but feel free to ask if it isn't clear where files go, whether website scripts need to be changed, etc.
Semi-relatedly, someone recently asked on Mastodon what a good source for the constructive ordinals is. There have been three suggestions so far. One is a normal math book (the HoTT book). The other two are collections of formalized proofs (iset.mm and TypeToplogy). And neither of the latter two give you an especially good idea of where to find the ordinal stuff and where to start. It got me thinking about how to make the material we have easy to read especially in cases where noone has written a textbook which lays everything out carefully with the purpose of teaching. Anyway, the thread is https://mathstodon.xyz/@boarders/110646213816213644 in case anyone is interested.
-- 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/b189ded2-5b48-ce91-fbfb-24edbbe011c7%40panix.com.
