$( This is the Metamath database iset.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 http://us.metamath.org and https://github.com/metamath/set.mm, and feel free to ask questions at http://groups.google.com/group/metamath. $) $( New users may want to read http://us.metamath.org/ileuni/conventions.html to understand the label naming conventions used in iset.mm. See also "help verify markup" in the Metamath program for markup conventions. $) $( To break this file into smaller modules, in the Metamath program type "read iset.mm" followed by "write source iset.mm /split"; to recombine, omit "/split". $) $( The database iset.mm was created by Mario Carneiro on 21-Jan-2015 from a fork of the database set.mm and has been continuously enriched since then (list of contributors below). Many additions and updates included copying entire theorems and sections from set.mm in order to keep some consistency among these databases. $) $( ! #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# Metamath source file for intuitionistic logic and set theory #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# ~~ PUBLIC DOMAIN ~~ This work is waived of all rights, including copyright, according to the CC0 Public Domain Dedication. http://creativecommons.org/publicdomain/zero/1.0/ Currently active maintainers: See the list in the CONTRIBUTING.md file. Contributor list: DA David Abernethy SA Stefan Allan TA Thierry Arnoux JA Juha Arpiainen JB Jonathan Ben-Naim GB Gregory Bush MC Mario Carneiro PC Paul Chapman DF Drahflow GD Georgy Dunaev SF Scott Fenton JGH Jeff Hankins AH Anthony Hart DH David Harvey CH Chen-Pang He JH Jeff Hoffman SJ Szymon Jaroszewicz BJ Benoit Jubin JK Jim Kingdon WL Wolf Lammen GL Gerard Lang BL Brendan Leahy RL Raph Levien FL Frederic Line RFL Roy F. Longton JM Jeff Madsen RM Rodolfo Medina NM Norman Megill JMG Jia Ming MM Mykola Mostovenko MO Mel L. O'Cat SO Stefan O'Rear JO Jason Orendorff JP Josh Purinton SR Steve Rodriguez ATS Andrew Salmon AS Alan Sare ES Eric Schmidt GS Glauco Siliprandi SS Saveliy Skresanov JU Jarvin Udandy AV Alexander van der Vekens DAW David A. Wheeler JY Jonathan Yan FZ Fan Zheng =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Contents of this header =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 1. Naming 2. Quick "How To" 3. Bibliography 4. Metamath syntax summary 5. Other notes 6. Acceptable shorter proofs =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 1. Naming =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Theorems which are the same as in set.mm should be named the same (that is, where the statement of the theorem is the same; the proof can differ without a new name being called for). Theorems which are different should be named differently (although if additional hypotheses are added in iset.mm the name need not be changed). As with set.mm, we welcome suggestions for better names (such as names which are more consistent with naming conventions). We do try to keep set.mm and iset.mm similar where we can. For example, if a theorem exists both places but the name in set.mm isn't great, we tend to keep that name for iset.mm, or change it in both files together. This is mainly to make it easier to copy theorems, but also to generally help people browse proofs, find theorems, write proofs, etc. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 2. Quick "How To" =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= How to use this file under Windows 95/98/NT/2K/XP/Vista: 1. Download the program metamath.exe per the instructions on the Metamath home page (http://us.metamath.org) and put it in the same directory as this file (set.mm). 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. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 3. Bibliography =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Bibliographical references are made by bracketing an identifer in a theorem's comment, such as [RussellWhitehead]. These refer to HTML tags on the following web pages: Logic and set theory - see http://us.metamath.org/mpegif/mmset.html#bib Hilbert space - see http://us.metamath.org/mpegif/mmhil.html#ref =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 4. Metamath syntax summary =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= The HELP LANGUAGE command in the Metamath program will give you a quick overview of Metamath. Syntax summary: $c ... $. - Constant declaration $v ... $. - Variable declaration $d ... $. - Disjoint (distinct) variable restriction