Home | Intuitionistic Logic Explorer Theorem List (p. 99 of 102) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description | ||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||
Theorem | climrel 9801 | The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | clim 9802* | Express the predicate: The limit of complex number sequence is , or converges to . This means that for any real , no matter how small, there always exists an integer such that the absolute difference of any later complex number in the sequence and the limit is less than . (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) | ||||||||||||
Theorem | climcl 9803 | Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) | ||||||||||||
Theorem | clim2 9804* | Express the predicate: The limit of complex number sequence is , or converges to , with more general quantifier restrictions than clim 9802. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | clim2c 9805* | Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | clim0 9806* | Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | clim0c 9807* | Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climi 9808* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climi2 9809* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climi0 9810* | Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climconst 9811* | An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climconst2 9812 | A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climz 9813 | The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climuni 9814 | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | fclim 9815 | The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climdm 9816 | Two ways to express that a function has a limit. (The expression is sometimes useful as a shorthand for "the unique limit of the function "). (Contributed by Mario Carneiro, 18-Mar-2014.) | ||||||||||||
Theorem | climeu 9817* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) | ||||||||||||
Theorem | climreu 9818* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) | ||||||||||||
Theorem | climmo 9819* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.) | ||||||||||||
Theorem | climeq 9820* | Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climmpt 9821* | Exhibit a function with the same convergence properties as the not-quite-function . (Contributed by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | 2clim 9822* | If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climshftlemg 9823 | A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.) | ||||||||||||
Theorem | climres 9824 | A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climshft 9825 | A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | iserclim0 9826 | The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.) | ||||||||||||
Theorem | climshft2 9827* | A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.) | ||||||||||||
Theorem | climabs0 9828* | Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climcn1 9829* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climcn2 9830* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | addcn2 9831* | Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcn for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | subcn2 9832* | Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | mulcn2 9833* | Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | cn1lem 9834* | A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | abscn2 9835* | The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | cjcn2 9836* | The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | recn2 9837* | The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | imcn2 9838* | The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | climcn1lem 9839* | The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | climabs 9840* | Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | climcj 9841* | Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | climre 9842* | Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | climim 9843* | Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | climrecl 9844* | The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.) | ||||||||||||
Theorem | climge0 9845* | A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.) | ||||||||||||
Theorem | climadd 9846* | Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.) | ||||||||||||
Theorem | climmul 9847* | Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.) | ||||||||||||
Theorem | climsub 9848* | Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.) | ||||||||||||
Theorem | climaddc1 9849* | Limit of a constant added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.) | ||||||||||||
Theorem | climaddc2 9850* | Limit of a constant added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.) | ||||||||||||
Theorem | climmulc2 9851* | Limit of a sequence multiplied by a constant . Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.) | ||||||||||||
Theorem | climsubc1 9852* | Limit of a constant subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | climsubc2 9853* | Limit of a constant minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.) | ||||||||||||
Theorem | climle 9854* | Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.) | ||||||||||||
Theorem | climsqz 9855* | Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.) | ||||||||||||
Theorem | climsqz2 9856* | Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.) | ||||||||||||
Theorem | clim2iser 9857* | The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.) | ||||||||||||
Theorem | clim2iser2 9858* | The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.) | ||||||||||||
Theorem | iiserex 9859* | An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.) | ||||||||||||
Theorem | iisermulc2 9860* | Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.) | ||||||||||||
Theorem | climlec2 9861* | Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.) | ||||||||||||
Theorem | iserile 9862* | Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.) | ||||||||||||
Theorem | iserige0 9863* | The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.) | ||||||||||||
Theorem | climub 9864* | The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.) | ||||||||||||
Theorem | climserile 9865* | The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.) | ||||||||||||
Theorem | climcau 9866* | A converging sequence of complex numbers is a Cauchy sequence. The converse would require excluded middle or a different definition of Cauchy sequence (for example, fixing a rate of convergence as in climcvg1n 9869). Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.) | ||||||||||||
Theorem | climrecvg1n 9867* | A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within of the nth term, where is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.) | ||||||||||||
Theorem | climcvg1nlem 9868* | Lemma for climcvg1n 9869. We construct sequences of the real and imaginary parts of each term of , show those converge, and use that to show that converges. (Contributed by Jim Kingdon, 24-Aug-2021.) | ||||||||||||
Theorem | climcvg1n 9869* | A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within of the nth term, where is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.) | ||||||||||||
Theorem | climcaucn 9870* | A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 9866 but adds the part that is complex. (Contributed by Jim Kingdon, 24-Aug-2021.) | ||||||||||||
Theorem | serif0 9871* | If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.) | ||||||||||||
Syntax | csu 9872 | Extend class notation to include finite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.) | ||||||||||||
Definition | df-sum 9873* | Define the sum of a series with an index set of integers . is normally a free variable in , i.e. can be thought of as . This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers). Examples: means , and means 1/2 + 1/4 + 1/8 + ... = 1. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) | ||||||||||||
Theorem | sumeq1 9874 | Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) | ||||||||||||
Theorem | nfsum1 9875 | Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) | ||||||||||||
Theorem | nfsum 9876 | Bound-variable hypothesis builder for sum: if is (effectively) not free in and , it is not free in . (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) | ||||||||||||
Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory. | ||||||||||||||
Theorem | sqr2irrlem 9877 | Lemma concerning rationality of square root of 2. The core of the proof - if , then and are even, so and are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) | ||||||||||||
Theorem | sqrt2irr 9878 |
The square root of 2 is not rational. That is, for any rational number,
does not equal it. However, if we were to say "the
square root of 2 is irrational" that would mean something stronger:
"for any rational number, is apart from it" (the two
statements are equivalent given excluded middle). We do not prove
irrationality in this stronger sense here.
The proof's core is proven in sqr2irrlem 9877, which shows that if , then and are even, so and are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) | ||||||||||||
Theorem | sqrt2re 9879 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) | ||||||||||||
Theorem | nn0seqcvgd 9880* | A strictly-decreasing nonnegative integer sequence with initial term reaches zero by the th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
Theorem | ialgrlem1st 9881 | Lemma for ialgr0 9883. Expressing algrflemg 5851 in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.) | ||||||||||||
Theorem | ialgrlemconst 9882 | Lemma for ialgr0 9883. Closure of a constant function, in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.) | ||||||||||||
Theorem | ialgr0 9883 | The value of the algorithm iterator at is the initial state . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) | ||||||||||||
Theorem | ialgrf 9884 |
An algorithm is a step function on a state space .
An algorithm acts on an initial state by
iteratively applying
to give , , and so
on. An algorithm is said to halt if a fixed point of is reached
after a finite number of iterations.
The algorithm iterator "runs" the algorithm so that is the state after iterations of on the initial state . Domain and codomain of the algorithm iterator . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) | ||||||||||||
Theorem | ialgrp1 9885 | The value of the algorithm iterator at . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) | ||||||||||||
Theorem | ialginv 9886* | If is an invariant of , its value is unchanged after any number of iterations of . (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
Theorem | ialgcvg 9887* |
One way to prove that an algorithm halts is to construct a countdown
function whose value is guaranteed to decrease for
each iteration of until it reaches . That is, if
is not a fixed point of , then
.
If is a countdown function for algorithm , the sequence reaches after at most steps, where is the value of for the initial state . (Contributed by Paul Chapman, 22-Jun-2011.) | ||||||||||||
Theorem | algcvgblem 9888 | Lemma for algcvgb 9889. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
Theorem | algcvgb 9889 | Two ways of expressing that is a countdown function for algorithm . The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011.) | ||||||||||||
Theorem | ialgcvga 9890* | The countdown function remains after steps. (Contributed by Paul Chapman, 22-Jun-2011.) | ||||||||||||
Theorem | ialgfx 9891* | If reaches a fixed point when the countdown function reaches , remains fixed after steps. (Contributed by Paul Chapman, 22-Jun-2011.) | ||||||||||||
This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:
| ||||||||||||||
Theorem | conventions 9892 |
Unless there is a reason to diverge, we follow the conventions of
the Metamath Proof Explorer (aka "set.mm"). This list of
conventions is intended to be read in conjunction with the
corresponding conventions in the Metamath Proof Explorer, and
only the differences are described below.
Label naming conventions Here are a few of the label naming conventions:
The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.
(Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
Theorem | ex-or 9893 | Example for ax-io 630. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||
Theorem | ex-an 9894 | Example for ax-ia1 99. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||
Theorem | ex-fl 9895 | Example for df-fl 9114. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||
Theorem | ex-ceil 9896 | Example for df-ceil 9115. (Contributed by AV, 4-Sep-2021.) | ||||||||||||
⌈ ⌈ | ||||||||||||||
Theorem | mathbox 9897 |
(This theorem is a dummy placeholder for these guidelines. The name of
this theorem, "mathbox", is hard-coded into the Metamath
program to
identify the start of the mathbox section for web page generation.)
A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it. Guidelines: 1. If at all possible, please use only 0-ary class constants for new definitions. 2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website. 3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm. 4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed. Notes: 1. We may decide to move some theorems to the main part of set.mm for general use. 2. We may make changes to mathboxes to maintain the overall quality of set.mm. Normally we will let you know if a change might impact what you are working on. 3. If you use theorems from another user's mathbox, we don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let us know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.) | ||||||||||||
Theorem | ax1hfs 9898 | Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.) | ||||||||||||
Theorem | nnexmid 9899 | Double negation of excluded middle. Intuitionistic logic refutes the negation of excluded middle (but, of course, does not prove excluded middle) for any formula. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||
Theorem | nndc 9900 | Double negation of decidability of a formula. Intuitionistic logic refutes undecidability (but, of course, does not prove decidability) of any formula. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||
DECID |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |