$( This is the Metamath database set.mm. $) $( Metamath is a formal language and associated computer program for archiving, verifying, and studying mathematical proofs, created by Norman Dwight Megill (1950--2021). For more information, visit https://us.metamath.org and https://github.com/metamath/set.mm, and feel free to ask questions at https://groups.google.com/g/metamath. $) $( New users may want to read https://us.metamath.org/mpeuni/conventions.html to understand the label naming conventions used in set.mm. See also the Metamath program command "MM> HELP VERIFY MARKUP" for markup conventions. $) $( To break this file into smaller modules, in the Metamath program type "MM> READ set.mm" followed by "MM> WRITE SOURCE set.mm / SPLIT". To recombine, omit "/ SPLIT". $) $( The database set.mm was created by Norman Megill on 30-Sep-1992 and has been continuously enriched since then (list of contributors below). $) $( ! #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# Metamath source file for logic and set theory #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# ~~ PUBLIC DOMAIN ~~ This work is waived of all rights, including copyright, according to the CC0 Public Domain Dedication. https://creativecommons.org/publicdomain/zero/1.0/ Currently active maintainers: See the list in the CONTRIBUTING.md file of https://github.com/metamath/set.mm. Contributor list: DA David Abernethy SA Stefan Allan TA Thierry Arnoux JA Juha Arpiainen JB Jonathan Ben-Naim GB Gregory Bush MC Mario Carneiro FC Filip Cernatescu PC Paul Chapman DF Drahflow AD Adrian Ducourtial GD Georgy Dunaev SF Scott Fenton GG Gino Giotto JGH Jeff Hankins AH Anthony Hart DH David Harvey CH Chen-Pang He JH Jeff Hoffman II Igor Ieskov AI Asger C. Ipsen JJ Jerry James SJ Szymon Jaroszewicz BJ Benoit Jubin JK Jim Kingdon ML M L WL Wolf Lammen GL Gerard Lang BL Brendan Leahy LL Larry Lesyna RL Raph Levien FL Frederic Line RFL Roy F. Longton JPM Jeffrey P. Machado JM Jeff Madsen GM Giovanni Mascellani PM Peter Mazsa RM Rodolfo Medina NM Norman Megill MKU metakunt DM David Moews MM Mykola Mostovenko SN Steven Nguyen MO Mel L. O'Cat OAI OpenAI SO Stefan O'Rear JO Jason Orendorff KP K P NP Noam Pasman JPP Jon Pennant RP Richard Penner SP Stanislas Polu JP Josh Purinton RMI Remi RR Rohan Ridenour SR Steve Rodriguez ATS Andrew Salmon AS Alan Sare ES Eric Schmidt GS Glauco Siliprandi SS Saveliy Skresanov BT BTernaryTau ET Ender Ting JU Jarvin Udandy ADH Stijn "Adhemar" Vandamme AV Alexander van der Vekens JV Jannik Vierling ZW Zhi Wang EW Emmett Weisz DAW David A. Wheeler RW Roger Witte KW Kyle Wyonch JY Jonathan Yan FZ Fan Zheng KZ Kunhao Zheng HTML code for accented names: BJ Benoît Jubin GL Gérard Lang FL Frédéric Liné $) $( See "MM> HELP VERIFY MARKUP" for help with modularization tags. $) $( Begin $[ set-header.mm $] $) $( ! =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Contents of this header =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= * Quick "How To" * Bibliography * Metamath syntax summary * Other notes =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Quick "How To" =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= How to use this file under Windows 95/98/NT/2K/XP/Vista/7/10: 1. Download the Metamath program metamath.exe following the instructions on the Metamath home page (https://us.metamath.org) and put it in the same directory as this file. 2. In Windows Explorer, double-click on metamath.exe. 3. Type "read set.mm" and press Enter. 4. Type "help" for a list of help topics, and "help demo" for some command examples. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Bibliography =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Bibliographical references are made by bracketing an identifier in a theorem's comment, such as [RussellWhitehead]. These refer to HTML tags on the following web pages: Logic and set theory - see https://us.metamath.org/mpeuni/mmset.html#bib Hilbert space - see https://us.metamath.org/mpeuni/mmhil.html#ref A bracketed reference must be preceded by a theorem number, etc. and followed by a page number. See "MM> HELP WRITE BIBLIOGRAPHY" for details. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Metamath syntax summary =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= The HELP LANGUAGE command in the Metamath program will give you a quick overview of Metamath. The specification is found on pp. 111--114 of the Metamath book. The following syntax summary is provided for convenience but may omit some details. A Metamath database (set of one or more ASCII source files) is a sequence of _tokens_, which are normally separated by spaces or line breaks. The only tokens that are built into the Metamath language are those (two-character sequences) beginning with $, shown in the following. These tokens are called _keywords_: $c ... $. - Constant declaration $v ... $. - Variable declaration $d ... $. - Disjoint (distinct) variable restriction