Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
4-Apr-2024 | prodrbdclem 11333 | Lemma for prodrbdc 11336. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.) |
DECID | ||
24-Mar-2024 | prodfdivap 11309 | The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
# | ||
24-Mar-2024 | prodfrecap 11308 | The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
# | ||
23-Mar-2024 | prodfap0 11307 | The product of finitely many terms apart from zero is apart from zero. (Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon, 23-Mar-2024.) |
# # | ||
22-Mar-2024 | prod3fmul 11303 | The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.) |
21-Mar-2024 | df-proddc 11313 | Define the product of a series with an index set of integers . This definition takes most of the aspects of df-sumdc 11116 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 21-Mar-2024.) |
DECID # | ||
19-Mar-2024 | cos02pilt1 12921 | Cosine is less than one between zero and . (Contributed by Jim Kingdon, 19-Mar-2024.) |
19-Mar-2024 | cosq34lt1 12920 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.) |
14-Mar-2024 | coseq0q4123 12904 | Location of the zeroes of cosine in . (Contributed by Jim Kingdon, 14-Mar-2024.) |
14-Mar-2024 | cosq23lt0 12903 | The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.) |
9-Mar-2024 | pilem3 12853 | Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.) |
9-Mar-2024 | exmidonfin 7043 | If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6759 and nnon 4518. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
EXMID | ||
9-Mar-2024 | exmidonfinlem 7042 | Lemma for exmidonfin 7043. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
DECID | ||
8-Mar-2024 | sin0pilem2 12852 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
8-Mar-2024 | sin0pilem1 12851 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
7-Mar-2024 | cosz12 12850 | Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.) |
6-Mar-2024 | cos12dec 11463 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) |
25-Feb-2024 | mul2lt0pn 9544 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
25-Feb-2024 | mul2lt0np 9543 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
25-Feb-2024 | lt0ap0 8403 | A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
# | ||
25-Feb-2024 | negap0d 8386 | The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
# # | ||
24-Feb-2024 | lt0ap0d 8404 | A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.) |
# | ||
20-Feb-2024 | ivthdec 12780 | The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.) |
20-Feb-2024 | ivthinclemex 12778 | Lemma for ivthinc 12779. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.) |
19-Feb-2024 | ivthinclemuopn 12774 | Lemma for ivthinc 12779. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.) |
19-Feb-2024 | dedekindicc 12769 | A Dedekind cut identifies a unique real number. Similar to df-inp 7267 except that the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 19-Feb-2024.) |
18-Feb-2024 | ivthinclemloc 12777 | Lemma for ivthinc 12779. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemdisj 12776 | Lemma for ivthinc 12779. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemur 12775 | Lemma for ivthinc 12779. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemlr 12773 | Lemma for ivthinc 12779. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemum 12771 | Lemma for ivthinc 12779. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemlm 12770 | Lemma for ivthinc 12779. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
15-Feb-2024 | dedekindicclemeu 12767 | Lemma for dedekindicc 12769. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemlu 12766 | Lemma for dedekindicc 12769. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemlub 12765 | Lemma for dedekindicc 12769. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemloc 12764 | Lemma for dedekindicc 12769. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemub 12763 | Lemma for dedekindicc 12769. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemuub 12762 | Lemma for dedekindicc 12769. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.) |
14-Feb-2024 | suplociccex 12761 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7830 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.) |
14-Feb-2024 | suplociccreex 12760 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7830 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.) |
6-Feb-2024 | ivthinclemlopn 12772 | Lemma for ivthinc 12779. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.) |
5-Feb-2024 | ivthinc 12779 | The intermediate value theorem, increasing case, for a strictly monotonic function. Theorem 5.5 of [Bauer], p. 494. This is Metamath 100 proof #79. (Contributed by Jim Kingdon, 5-Feb-2024.) |
2-Feb-2024 | dedekindeulemuub 12753 | Lemma for dedekindeu 12759. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.) |
31-Jan-2024 | dedekindeulemeu 12758 | Lemma for dedekindeu 12759. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemlu 12757 | Lemma for dedekindeu 12759. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemlub 12756 | Lemma for dedekindeu 12759. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemloc 12755 | Lemma for dedekindeu 12759. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemub 12754 | Lemma for dedekindeu 12759. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
30-Jan-2024 | axsuploc 7830 | An inhabited, bounded-above, located set of reals has a supremum. Axiom for real and complex numbers, derived from ZF set theory. (This restates ax-pre-suploc 7734 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) |
24-Jan-2024 | axpre-suploclemres 7702 | Lemma for axpre-suploc 7703. The result. The proof just needs to define as basically the same set as (but expressed as a subset of rather than a subset of ), and apply suplocsr 7610. (Contributed by Jim Kingdon, 24-Jan-2024.) |
23-Jan-2024 | ax-pre-suploc 7734 |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given , either there is an element of the set greater than , or is an upper bound. Although this and ax-caucvg 7733 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7733. (Contributed by Jim Kingdon, 23-Jan-2024.) |
23-Jan-2024 | axpre-suploc 7703 |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given , either there is an element of the set greater than , or is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7734. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
22-Jan-2024 | suplocsr 7610 | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) |
21-Jan-2024 | bj-el2oss1o 12970 | Shorter proof of el2oss1o 13177 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
21-Jan-2024 | ltm1sr 7578 | Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.) |
19-Jan-2024 | suplocsrlempr 7608 | Lemma for suplocsr 7610. The set has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.) |
18-Jan-2024 | suplocsrlemb 7607 | Lemma for suplocsr 7610. The set is located. (Contributed by Jim Kingdon, 18-Jan-2024.) |
16-Jan-2024 | suplocsrlem 7609 | Lemma for suplocsr 7610. The set has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.) |
14-Jan-2024 | suplocexprlemlub 7525 | Lemma for suplocexpr 7526. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
14-Jan-2024 | suplocexprlemub 7524 | Lemma for suplocexpr 7526. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
10-Jan-2024 | cbvcsbw 3002 | Version of cbvcsb 3003 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbvsbcw 2931 | Version of cbvsbc 2932 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbvabw 2260 | Version of cbvab 2261 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) |
9-Jan-2024 | suplocexprlemloc 7522 | Lemma for suplocexpr 7526. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemdisj 7521 | Lemma for suplocexpr 7526. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemru 7520 | Lemma for suplocexpr 7526. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemrl 7518 | Lemma for suplocexpr 7526. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlem2b 7515 | Lemma for suplocexpr 7526. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemell 7514 | Lemma for suplocexpr 7526. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
7-Jan-2024 | suplocexpr 7526 | An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemex 7523 | Lemma for suplocexpr 7526. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemmu 7519 | Lemma for suplocexpr 7526. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemml 7517 | Lemma for suplocexpr 7526. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemss 7516 | Lemma for suplocexpr 7526. is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.) |
5-Jan-2024 | dedekindicclemicc 12768 | Lemma for dedekindicc 12769. Same as dedekindicc 12769, except that we merely show to be an element of . Later we will strengthen that to . (Contributed by Jim Kingdon, 5-Jan-2024.) |
5-Jan-2024 | dedekindeu 12759 | A Dedekind cut identifies a unique real number. Similar to df-inp 7267 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.) |
31-Dec-2023 | dvmptsubcn 12843 | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
31-Dec-2023 | dvmptnegcn 12842 | Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
31-Dec-2023 | dvmptcmulcn 12841 | Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
31-Dec-2023 | brm 3973 | If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.) |
30-Dec-2023 | dvmptccn 12837 | Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.) |
30-Dec-2023 | dvmptidcn 12836 | Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.) |
25-Dec-2023 | ctfoex 6996 | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊔ | ||
23-Dec-2023 | enct 11935 | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
23-Dec-2023 | enctlem 11934 | Lemma for enct 11935. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
23-Dec-2023 | omct 6995 | is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ | ||
21-Dec-2023 | dvcoapbr 12829 | The chain rule for derivatives at a point. The # # hypothesis constrains what functions work for . (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.) |
# # | ||
19-Dec-2023 | apsscn 8402 | The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.) |
# | ||
19-Dec-2023 | aprcl 8401 | Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.) |
# | ||
18-Dec-2023 | limccoap 12805 | Composition of two limits. This theorem is only usable in the case where # implies R(x) # so it is less general than might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.) (Revised by Jim Kingdon, 18-Dec-2023.) |
# # # # lim # lim # lim | ||
16-Dec-2023 | cnreim 10743 | Complex apartness in terms of real and imaginary parts. See also apreim 8358 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) |
# # # | ||
14-Dec-2023 | cnopnap 12752 | The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.) |
# | ||
14-Dec-2023 | cnovex 12354 | The class of all continuous functions from a topology to another is a set. (Contributed by Jim Kingdon, 14-Dec-2023.) |
13-Dec-2023 | reopnap 12696 | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
# | ||
12-Dec-2023 | cnopncntop 12695 | The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.) |
12-Dec-2023 | unicntopcntop 12694 | The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.) |
4-Dec-2023 | bj-pm2.18st 12947 | Clavius law for stable formulas. See pm2.18dc 840. (Contributed by BJ, 4-Dec-2023.) |
STAB | ||
4-Dec-2023 | bj-nnclavius 12939 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) |
2-Dec-2023 | dvmulxx 12826 | The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 12824. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.) |
1-Dec-2023 | dvmulxxbr 12824 | The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 12826. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.) |
29-Nov-2023 | subctctexmid 13185 | If every subcountable set is countable and Markov's principle holds, excluded middle follows. Proposition 2.6 of [BauerSwan], p. 14:4. The proof is taken from that paper. (Contributed by Jim Kingdon, 29-Nov-2023.) |
⊔ Markov EXMID | ||
29-Nov-2023 | ismkvnex 7022 | The predicate of being Markov stated in terms of double negation and comparison with . (Contributed by Jim Kingdon, 29-Nov-2023.) |
Markov | ||
28-Nov-2023 | exmid1stab 13184 | If any proposition is stable, excluded middle follows. We are thinking of as a proposition and as "x is true". (Contributed by Jim Kingdon, 28-Nov-2023.) |
STAB EXMID | ||
28-Nov-2023 | ccfunen 7072 | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
CCHOICE | ||
27-Nov-2023 | df-cc 7071 | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7055 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
CCHOICE | ||
26-Nov-2023 | offeq 5988 | Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Jim Kingdon, 26-Nov-2023.) |
25-Nov-2023 | dvaddxx 12825 | The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 12823. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.) |
25-Nov-2023 | dvaddxxbr 12823 | The sum rule for derivatives at a point. That is, if the derivative of at is and the derivative of at is , then the derivative of the pointwise sum of those two functions at is . (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.) |
25-Nov-2023 | dcnn 833 | Decidability of the negation of a proposition is equivalent to decidability of its double negation. See also dcn 827. The relation between dcn 827 and dcnn 833 is analogous to that between notnot 618 and notnotnot 623 (and directly stems from it). Using the notion of "testable proposition" (proposition whose negation is decidable), dcnn 833 means that a proposition is testable if and only if its negation is testable, and dcn 827 means that decidability implies testability. (Contributed by David A. Wheeler, 6-Dec-2018.) (Proof shortened by BJ, 25-Nov-2023.) |
DECID DECID | ||
24-Nov-2023 | bj-dcst 12956 | Stability of a proposition is decidable if and only if that proposition is stable. (Contributed by BJ, 24-Nov-2023.) |
DECID STAB STAB | ||
24-Nov-2023 | bj-nnbidc 12951 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 12942. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-dcstab 12950 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) |
DECID STAB | ||
24-Nov-2023 | bj-fadc 12949 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-trdc 12948 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-stal 12946 | The universal quantification of stable formula is stable. See bj-stim 12943 for implication, stabnot 818 for negation, and bj-stan 12944 for conjunction. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB | ||
24-Nov-2023 | bj-stand 12945 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 12944. Its proof is shorter, so one could prove it first and then bj-stan 12944 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) |
STAB STAB STAB | ||
24-Nov-2023 | bj-stan 12944 | The conjunction of two stable formulas is stable. See bj-stim 12943 for implication, stabnot 818 for negation, and bj-stal 12946 for universal quantification. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB STAB | ||
24-Nov-2023 | bj-stim 12943 | A conjunction with a stable consequent is stable. See stabnot 818 for negation and bj-stan 12944 for conjunction. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB | ||
24-Nov-2023 | bj-nnbist 12942 | If a formula is not refutable, then it is stable if and only if it is provable. By double-negation translation, if is a classical tautology, then is an intuitionistic tautology. Therefore, if is a classical tautology, then is intuitionistically equivalent to its stability (and to its decidability, see bj-nnbidc 12951). (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-fast 12941 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-trst 12940 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-nnal 12938 | The double negation of a universal quantification implies the universal quantification of the double negation. (Contributed by BJ, 24-Nov-2023.) |
24-Nov-2023 | bj-nnan 12937 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) |
24-Nov-2023 | bj-nnim 12936 | The double negation of an implication implies the implication with the consequent doubly negated. (Contributed by BJ, 24-Nov-2023.) |
24-Nov-2023 | bj-nnsn 12934 | As far as implying a negated formula is concerned, a formula is equivalent to its double negation. (Contributed by BJ, 24-Nov-2023.) |
22-Nov-2023 | ofvalg 5984 | Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.) |
21-Nov-2023 | exmidac 7058 | The axiom of choice implies excluded middle. See acexmid 5766 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.) |
CHOICE EXMID | ||
21-Nov-2023 | exmidaclem 7057 | Lemma for exmidac 7058. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
CHOICE EXMID | ||
21-Nov-2023 | exmid1dc 4118 | A convenience theorem for proving that something implies EXMID. Think of this as an alternative to using a proposition, as in proofs like undifexmid 4112 or ordtriexmid 4432. In this context can be thought of as "x is true". (Contributed by Jim Kingdon, 21-Nov-2023.) |
DECID EXMID | ||
20-Nov-2023 | acfun 7056 | A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.) |
CHOICE | ||
18-Nov-2023 | condc 838 |
Contraposition of a decidable proposition.
This theorem swaps or "transposes" the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This theorem (without the decidability condition, of course) is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103) and is Axiom A3 of [Margaris] p. 49. We will also use the term "contraposition" for this principle, although the reader is advised that in the field of philosophical logic, "contraposition" has a different technical meaning. (Contributed by Jim Kingdon, 13-Mar-2018.) (Proof shortened by BJ, 18-Nov-2023.) |
DECID | ||
18-Nov-2023 | const 837 | Contraposition of a stable proposition. See comment of condc 838. (Contributed by BJ, 18-Nov-2023.) |
STAB | ||
18-Nov-2023 | stdcn 832 | A formula is stable if and only if the decidability of its negation implies its decidability. Note that the right-hand side of this biconditional is the converse of dcn 827. (Contributed by BJ, 18-Nov-2023.) |
STAB DECID DECID | ||
17-Nov-2023 | cnplimclemr 12796 | Lemma for cnplimccntop 12797. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) |
↾t lim | ||
17-Nov-2023 | cnplimclemle 12795 | Lemma for cnplimccntop 12797. Satisfying the epsilon condition for continuity. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) |
↾t lim # | ||
14-Nov-2023 | limccnp2cntop 12804 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Nov-2023.) |
↾t lim lim lim | ||
10-Nov-2023 | rpmaxcl 10988 | The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.) |
9-Nov-2023 | limccnp2lem 12803 | Lemma for limccnp2cntop 12804. This is most of the result, expressed in epsilon-delta form, with a large number of hypotheses so that lengthy expressions do not need to be repeated. (Contributed by Jim Kingdon, 9-Nov-2023.) |
↾t lim lim # # # | ||
4-Nov-2023 | ellimc3apf 12787 | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.) |
lim # | ||
3-Nov-2023 | limcmpted 12790 | Express the limit operator for a function defined by a mapping, via epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.) |
lim # | ||
1-Nov-2023 | unct 11943 | The union of two countable sets is countable. (Contributed by Jim Kingdon, 1-Nov-2023.) |
⊔ ⊔ ⊔ | ||
31-Oct-2023 | ctiunct 11942 |
A sequence of enumerations gives an enumeration of the union. We refer
to "sequence of enumerations" rather than "countably many
countable
sets" because the hypothesis provides more than countability for
each
: it refers to together with the
which enumerates it.
The "countably many countable sets" version could be expressed as ⊔ and countable choice would be needed to derive the current hypothesis from that. Compare with the case of two sets instead of countably many, as seen at unct 11943, in which case we express countability using . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 11897) and using the first number to map to an element of and the second number to map to an element of B(x) . In this way we are able to map to every element of . Although it would be possible to work directly with countability expressed as ⊔ , we instead use functions from subsets of the natural numbers via ctssdccl 6989 and ctssdc 6991. (Contributed by Jim Kingdon, 31-Oct-2023.) |
⊔ ⊔ ⊔ | ||
30-Oct-2023 | ctssdccl 6989 | A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 6991 but expressed in terms of classes rather than . (Contributed by Jim Kingdon, 30-Oct-2023.) |
⊔ inl inl DECID | ||
28-Oct-2023 | ctiunctlemfo 11941 | Lemma for ctiunct 11942. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | ctiunctlemf 11940 | Lemma for ctiunct 11942. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | ctiunctlemudc 11939 | Lemma for ctiunct 11942. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID DECID | ||
28-Oct-2023 | ctiunctlemuom 11938 | Lemma for ctiunct 11942. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | ctiunctlemu2nd 11937 | Lemma for ctiunct 11942. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | ctiunctlemu1st 11936 | Lemma for ctiunct 11942. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | pm2.521gdc 853 | A general instance of Theorem *2.521 of [WhiteheadRussell] p. 107, under a decidability condition. (Contributed by BJ, 28-Oct-2023.) |
DECID | ||
28-Oct-2023 | stdcndc 830 | A formula is decidable if and only if its negation is decidable and it is stable (that is, it is testable and stable). (Contributed by David A. Wheeler, 13-Aug-2018.) (Proof shortened by BJ, 28-Oct-2023.) |
STAB DECID DECID | ||
28-Oct-2023 | conax1k 643 | Weakening of conax1 642. General instance of pm2.51 644 and of pm2.52 645. (Contributed by BJ, 28-Oct-2023.) |
28-Oct-2023 | conax1 642 | Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.) |
25-Oct-2023 | divcnap 12713 | Complex number division is a continuous function, when the second argument is apart from zero. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Jim Kingdon, 25-Oct-2023.) |
↾t # # | ||
23-Oct-2023 | cnm 7633 | A complex number is an inhabited set. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by Jim Kingdon, 23-Oct-2023.) (New usage is discouraged.) |
23-Oct-2023 | oprssdmm 6062 | Domain of closure of an operation. (Contributed by Jim Kingdon, 23-Oct-2023.) |
22-Oct-2023 | addcncntoplem 12709 | Lemma for addcncntop 12710, subcncntop 12711, and mulcncntop 12712. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) |
22-Oct-2023 | txmetcnp 12676 | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.) |
22-Oct-2023 | xmetxpbl 12666 | The maximum metric (Chebyshev distance) on the product of two sets, expressed in terms of balls centered on a point with radius . (Contributed by Jim Kingdon, 22-Oct-2023.) |
15-Oct-2023 | xmettxlem 12667 | Lemma for xmettx 12668. (Contributed by Jim Kingdon, 15-Oct-2023.) |
11-Oct-2023 | xmettx 12668 | The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.) |
11-Oct-2023 | xmetxp 12665 | The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.) |
12-Sep-2023 | pwntru 4117 | A slight strengthening of pwtrufal 13181. (Contributed by Mario Carneiro and Jim Kingdon, 12-Sep-2023.) |
11-Sep-2023 | pwtrufal 13181 | A subset of the singleton cannot be anything other than or . Removing the double negation would change the meaning, as seen at exmid01 4116. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4115), then this theorem states there are no truth values other than true and false, as described in section 1.1 of [Bauer], p. 481. (Contributed by Mario Carneiro and Jim Kingdon, 11-Sep-2023.) |
9-Sep-2023 | mathbox 12933 |
(This theorem is a dummy placeholder for these guidelines. The label
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 iset.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of iset.mm. Guidelines: Mathboxes in iset.mm follow the same practices as in set.mm, so refer to the mathbox guidelines there for more details. (Contributed by NM, 20-Feb-2007.) (Revised by the Metamath team, 9-Sep-2023.) (New usage is discouraged.) |
6-Sep-2023 | djuexb 6922 | The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.) |
⊔ | ||
3-Sep-2023 | pwf1oexmid 13183 | An exercise related to copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.) |
EXMID | ||
3-Sep-2023 | pwle2 13182 | An exercise related to copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.) |
30-Aug-2023 | isomninn 13215 | Omniscience stated in terms of natural numbers. Similar to isomnimap 7002 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 30-Aug-2023.) |
Omni | ||
30-Aug-2023 | isomninnlem 13214 | Lemma for isomninn 13215. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.) |
frec Omni | ||
28-Aug-2023 | trilpolemisumle 13220 | Lemma for trilpo 13225. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.) |
25-Aug-2023 | cvgcmp2n 13217 | A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.) |
25-Aug-2023 | cvgcmp2nlemabs 13216 | Lemma for cvgcmp2n 13217. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting as the sum of and a term which gets smaller as gets large. (Contributed by Jim Kingdon, 25-Aug-2023.) |
24-Aug-2023 | trilpolemclim 13218 | Lemma for trilpo 13225. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.) |
23-Aug-2023 | trilpo 13225 |
Real number trichotomy implies the Limited Principle of Omniscience
(LPO). We expect that we'd need some form of countable choice to prove
the converse.
Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence contains a zero or it is all ones. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. Compare it with one using trichotomy. The three cases from trichotomy are trilpolemlt1 13223 (which means the sequence contains a zero), trilpolemeq1 13222 (which means the sequence is all ones), and trilpolemgt1 13221 (which is not possible). (Contributed by Jim Kingdon, 23-Aug-2023.) |
Omni | ||
23-Aug-2023 | trilpolemres 13224 | Lemma for trilpo 13225. The result. (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | trilpolemlt1 13223 | Lemma for trilpo 13225. The case. We can use the distance between and one (that is, ) to find a position in the sequence where terms after that point will not add up to as much as . By finomni 7005 we know the terms up to either contain a zero or are all one. But if they are all one that contradicts the way we constructed , so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | trilpolemeq1 13222 | Lemma for trilpo 13225. The case. This is proved by noting that if any is zero, then the infinite sum is less than one based on the term which is zero. We are using the fact that the sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | trilpolemgt1 13221 | Lemma for trilpo 13225. The case. (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | trilpolemcl 13219 | Lemma for trilpo 13225. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | triap 13213 | Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.) |
DECID # | ||
19-Aug-2023 | djuenun 7061 | Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.) |
⊔ | ||
16-Aug-2023 | ctssdclemr 6990 | Lemma for ctssdc 6991. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊔ DECID | ||
16-Aug-2023 | ctssdclemn0 6988 | Lemma for ctssdc 6991. The case. (Contributed by Jim Kingdon, 16-Aug-2023.) |
DECID ⊔ | ||
15-Aug-2023 | ctssexmid 7017 | The decidability condition in ctssdc 6991 is needed. More specifically, ctssdc 6991 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊔ Omni | ||
15-Aug-2023 | ctssdc 6991 | A set is countable iff there is a surjection from a decidable subset of the natural numbers onto it. The decidability condition is needed as shown at ctssexmid 7017. (Contributed by Jim Kingdon, 15-Aug-2023.) |
DECID ⊔ | ||
13-Aug-2023 | ltntri 7883 | Negative trichotomy property for real numbers. It is well known that we cannot prove real number trichotomy, . Does that mean there is a pair of real numbers where none of those hold (that is, where we can refute each of those three relationships)? Actually, no, as shown here. This is another example of distinguishing between being unable to prove something, or being able to refute it. (Contributed by Jim Kingdon, 13-Aug-2023.) |
13-Aug-2023 | nfsbv 1918 | If is not free in , it is not free in when is distinct from and . Version of nfsb 1917 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on . (Revised by Steven Nguyen, 13-Aug-2023.) |
11-Aug-2023 | qnnen 11933 | The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.) |
10-Aug-2023 | ctinfomlemom 11929 | Lemma for ctinfom 11930. Converting between and . (Contributed by Jim Kingdon, 10-Aug-2023.) |
frec | ||
9-Aug-2023 | difinfsnlem 6977 | Lemma for difinfsn 6978. The case where we need to swap and inr in building the mapping . (Contributed by Jim Kingdon, 9-Aug-2023.) |
DECID ⊔ inr inl inr inl | ||
8-Aug-2023 | difinfinf 6979 | An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
DECID | ||
8-Aug-2023 | difinfsn 6978 | An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
DECID | ||
7-Aug-2023 | ctinf 11932 | A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
7-Aug-2023 | inffinp1 11931 | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
7-Aug-2023 | ctinfom 11930 | A condition for a set being countably infinite. Restates ennnfone 11927 in terms of and function image. Like ennnfone 11927 the condition can be summarized as being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
6-Aug-2023 | rerestcntop 12708 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.) |
↾t ↾t | ||
6-Aug-2023 | tgioo2cntop 12707 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.) |
↾t | ||
4-Aug-2023 | nninffeq 13205 | Equality of two functions on ℕ∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 4-Aug-2023.) |
ℕ∞ ℕ∞ | ||
3-Aug-2023 | txvalex 12412 | Existence of the binary topological product. If and are known to be topologies, see txtop 12418. (Contributed by Jim Kingdon, 3-Aug-2023.) |
3-Aug-2023 | dvdsgcdidd 11671 | The greatest common divisor of a positive integer and another integer it divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | gcdmultipled 11670 | The greatest common divisor of a nonnegative integer and a multiple of it is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | phpeqd 6814 | Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6752 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | enpr2d 6704 | A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | elrnmpt2d 4789 | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | elrnmptdv 4788 | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | rspcime 2791 | Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | neqcomd 2142 | Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
2-Aug-2023 | dvid 12820 | Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
2-Aug-2023 | dvconst 12819 | Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
2-Aug-2023 | dvidlemap 12818 | Lemma for dvid 12820 and dvconst 12819. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
# | ||
2-Aug-2023 | diveqap1bd 8588 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveqap1 8458. Converse of diveqap1d 8551. (Contributed by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.) |
# | ||
1-Aug-2023 | cnstab 8400 | Equality of complex numbers is stable. Stability here means as defined at df-stab 816. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) |
STAB | ||
31-Jul-2023 | mul0inf 11005 | Equality of a product with zero. A bit of a curiosity, in the sense that theorems like abs00ap 10827 and mulap0bd 8411 may better express the ideas behind it. (Contributed by Jim Kingdon, 31-Jul-2023.) |
inf | ||
31-Jul-2023 | mul0eqap 8424 | If two numbers are apart from each other and their product is zero, one of them must be zero. (Contributed by Jim Kingdon, 31-Jul-2023.) |
# | ||
31-Jul-2023 | apcon4bid 8379 | Contrapositive law deduction for apartness. (Contributed by Jim Kingdon, 31-Jul-2023.) |
# # | ||
30-Jul-2023 | uzennn 10202 | An upper integer set is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 30-Jul-2023.) |
30-Jul-2023 | djuen 7060 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ ⊔ | ||
30-Jul-2023 | endjudisj 7059 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ | ||
30-Jul-2023 | eninr 6976 | Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
inr | ||
30-Jul-2023 | eninl 6975 | Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
inl | ||
29-Jul-2023 | exmidunben 11928 | If any unbounded set of positive integers is equinumerous to , then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.) |
Omni EXMID | ||
29-Jul-2023 | exmidsssnc 4121 | Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4116 but lets you choose any set as the element of the singleton rather than just . It is similar to exmidsssn 4120 but for a particular set rather than all sets. (Contributed by Jim Kingdon, 29-Jul-2023.) |
EXMID | ||
28-Jul-2023 | dvfcnpm 12817 | The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.) |
28-Jul-2023 | dvfpm 12816 | The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.) |
23-Jul-2023 | ennnfonelemhdmp1 11911 | Lemma for ennnfone 11927. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
23-Jul-2023 | ennnfonelemp1 11908 | Lemma for ennnfone 11927. Value of at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
22-Jul-2023 | nntr2 6392 | Transitive law for natural numbers. (Contributed by Jim Kingdon, 22-Jul-2023.) |
22-Jul-2023 | nnsssuc 6391 | A natural number is a subset of another natural number if and only if it belongs to its successor. (Contributed by Jim Kingdon, 22-Jul-2023.) |
21-Jul-2023 | ennnfoneleminc 11913 | Lemma for ennnfone 11927. We only add elements to as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.) |
DECID frec | ||
20-Jul-2023 | ennnfonelemg 11905 | Lemma for ennnfone 11927. Closure for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
20-Jul-2023 | ennnfonelemjn 11904 | Lemma for ennnfone 11927. Non-initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
20-Jul-2023 | ennnfonelemj0 11903 | Lemma for ennnfone 11927. Initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
20-Jul-2023 | seqp1cd 10232 | Value of the sequence builder function at a successor. A version of seq3p1 10228 which provides two classes and for the terms and the value being accumulated, respectively. (Contributed by Jim Kingdon, 20-Jul-2023.) |
20-Jul-2023 | seqovcd 10229 | A closure law for the recursive sequence builder. This is a lemma for theorems such as seqf2 10230 and seq1cd 10231 and is unlikely to be needed once such theorems are proved. (Contributed by Jim Kingdon, 20-Jul-2023.) |
19-Jul-2023 | ennnfonelemhom 11917 | Lemma for ennnfone 11927. The sequences in increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | ennnfonelemex 11916 | Lemma for ennnfone 11927. Extending the sequence to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | ennnfonelemkh 11914 | Lemma for ennnfone 11927. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | ennnfonelemom 11910 | Lemma for ennnfone 11927. yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | ennnfonelem1 11909 | Lemma for ennnfone 11927. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | seq1cd 10231 | Initial value of the recursive sequence builder. A version of seq3-1 10226 which provides two classes and for the terms and the value being accumulated, respectively. (Contributed by Jim Kingdon, 19-Jul-2023.) |
17-Jul-2023 | ennnfonelemhf1o 11915 | Lemma for ennnfone 11927. Each of the functions in is one to one and onto an image of . (Contributed by Jim Kingdon, 17-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemen 11923 | Lemma for ennnfone 11927. The result. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemdm 11922 | Lemma for ennnfone 11927. The function is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemrn 11921 | Lemma for ennnfone 11927. is onto . (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemf1 11920 | Lemma for ennnfone 11927. is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemfun 11919 | Lemma for ennnfone 11927. is a function. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemrnh 11918 | Lemma for ennnfone 11927. A consequence of ennnfonelemss 11912. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
15-Jul-2023 | ennnfonelemss 11912 | Lemma for ennnfone 11927. We only add elements to as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
15-Jul-2023 | ennnfonelem0 11907 | Lemma for ennnfone 11927. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
15-Jul-2023 | ennnfonelemk 11902 | Lemma for ennnfone 11927. (Contributed by Jim Kingdon, 15-Jul-2023.) |
15-Jul-2023 | ennnfonelemdc 11901 | Lemma for ennnfone 11927. A direct consequence of fidcenumlemrk 6835. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID DECID | ||
14-Jul-2023 | djur 6947 | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) Upgrade implication to biconditional and shorten proof. (Revised by BJ, 14-Jul-2023.) |
⊔ inl inr | ||
13-Jul-2023 | sbthomlem 13209 | Lemma for sbthom 13210. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.) |
Omni ⊔ | ||
12-Jul-2023 | caseinr 6970 | Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.) |
case inr | ||
12-Jul-2023 | inl11 6943 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
inl inl | ||
11-Jul-2023 | djudomr 7069 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
11-Jul-2023 | djudoml 7068 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
11-Jul-2023 | omp1eomlem 6972 | Lemma for omp1eom 6973. (Contributed by Jim Kingdon, 11-Jul-2023.) |
inr inl case ⊔ | ||
11-Jul-2023 | xp01disjl 6324 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.) |
10-Jul-2023 | sbthom 13210 | Schroeder-Bernstein is not possible even for . We know by exmidsbth 13208 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is ? That case plus the Limited Principle of Omniscience (LPO) implies excluded middle, so we will not be able to prove it. (Contributed by Mario Carneiro and Jim Kingdon, 10-Jul-2023.) |
Omni EXMID | ||
10-Jul-2023 | endjusym 6974 | Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊔ ⊔ | ||
10-Jul-2023 | omp1eom 6973 | Adding one to . (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊔ | ||
9-Jul-2023 | refeq 13212 | Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.) |
9-Jul-2023 | seqvalcd 10225 | Value of the sequence builder function. Similar to seq3val 10224 but the classes (type of each term) and (type of the value we are accumulating) do not need to be the same. (Contributed by Jim Kingdon, 9-Jul-2023.) |
frec | ||
9-Jul-2023 | djuun 6945 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
inl inr ⊔ | ||
9-Jul-2023 | djuin 6942 | The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
inl inr | ||
8-Jul-2023 | limcimo 12792 | Conditions which ensure there is at most one limit value of at . (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 8-Jul-2023.) |
↾t # lim | ||
8-Jul-2023 | ennnfonelemh 11906 | Lemma for ennnfone 11927. (Contributed by Jim Kingdon, 8-Jul-2023.) |
DECID frec | ||
7-Jul-2023 | seqf2 10230 | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 7-Jul-2023.) |
3-Jul-2023 | limcimolemlt 12791 | Lemma for limcimo 12792. (Contributed by Jim Kingdon, 3-Jul-2023.) |
↾t # lim lim # # | ||
28-Jun-2023 | dvfgg 12815 | Explicitly write out the functionality condition on derivative for and . (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jun-2023.) |
28-Jun-2023 | dvbsssg 12813 | The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Jim Kingdon, 28-Jun-2023.) |
27-Jun-2023 | dvbssntrcntop 12811 | The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) |
↾t | ||
27-Jun-2023 | eldvap 12809 | The differentiable predicate. A function is differentiable at with derivative iff is defined in a neighborhood of and the difference quotient has limit at . (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) |
↾t # lim | ||
27-Jun-2023 | dvfvalap 12808 | Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) |
↾t # lim | ||
27-Jun-2023 | dvlemap 12807 | Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) |
# | ||
25-Jun-2023 | reldvg 12806 | The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.) |
25-Jun-2023 | df-dvap 12784 | Define the derivative operator. This acts on functions to produce a function that is defined where the original function is differentiable, with value the derivative of the function at these points. The set here is the ambient topological space under which we are evaluating the continuity of the difference quotient. Although the definition is valid for any subset of and is well-behaved when contains no isolated points, we will restrict our attention to the cases or for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.) |
↾t # lim | ||
18-Jun-2023 | limccnpcntop 12802 | If the limit of at is and is continuous at , then the limit of at is . (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 18-Jun-2023.) |
↾t lim lim | ||
17-Jun-2023 | r19.28v 2558 | Restricted quantifier version of one direction of 19.28 1542. (The other direction holds when is inhabited, see r19.28mv 3450.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
17-Jun-2023 | r19.27v 2557 | Restricted quantitifer version of one direction of 19.27 1540. (The other direction holds when is inhabited, see r19.27mv 3454.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
16-Jun-2023 | cnlimcim 12798 | If is a continuous function, the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 16-Jun-2023.) |
lim | ||
16-Jun-2023 | cncfcn1cntop 12739 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.) |
14-Jun-2023 | cnplimcim 12794 | If a function is continuous at , its limit at equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.) |
↾t lim | ||
14-Jun-2023 | metcnpd 12678 | Two ways to say a mapping from metric to metric is continuous at point . (Contributed by Jim Kingdon, 14-Jun-2023.) |
6-Jun-2023 | cntoptop 12691 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
6-Jun-2023 | cntoptopon 12690 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
TopOn | ||
3-Jun-2023 | limcdifap 12789 | It suffices to consider functions which are not defined at to define the limit of a function. In particular, the value of the original function at does not affect the limit of . (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.) |
lim # lim | ||
3-Jun-2023 | ellimc3ap 12788 | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon, 3-Jun-2023.) |
lim # | ||
3-Jun-2023 | df-limced 12783 | Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.) |
lim # | ||
29-May-2023 | mulcncflem 12748 | Lemma for mulcncf 12749. (Contributed by Jim Kingdon, 29-May-2023.) |
26-May-2023 | cdivcncfap 12745 | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.) |
# # | ||
26-May-2023 | reccn2ap 11075 | The reciprocal function is continuous. The class is just for convenience in writing the proof and typically would be passed in as an instance of eqid 2137. (Contributed by Mario Carneiro, 9-Feb-2014.) Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.) |
inf # # | ||
23-May-2023 | iooretopg 12686 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon, 23-May-2023.) |
23-May-2023 | minclpr 11001 | The minimum of two real numbers is one of those numbers if and only if dichotomy ( ) holds. For example, this can be combined with zletric 9091 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 23-May-2023.) |
inf | ||
22-May-2023 | qtopbasss 12679 | The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Jim Kingdon, 22-May-2023.) |
inf | ||
22-May-2023 | iooinsup 11039 | Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.) |
inf | ||
21-May-2023 | df-sumdc 11116 | 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. In both cases we have an expression so that we only need to be defined where . In the infinite case, we also require that the indexing set be a decidable subset of an upperset of integers (that is, membership of integers in it is decidable). These two methods of summation produce the same result on their common region of definition (i.e. finite sets of integers). Examples: means , and means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 11284). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.) |
DECID | ||
19-May-2023 | bdmopn 12662 | The standard bounded metric corresponding to generates the same topology as . (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.) |
inf | ||
19-May-2023 | bdbl 12661 | The standard bounded metric corresponding to generates the same balls as for radii less than . (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.) |
inf | ||
19-May-2023 | bdmet 12660 | The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.) |
inf | ||
19-May-2023 | xrminltinf 11034 | Two ways of saying an extended real is greater than the minimum of two others. (Contributed by Jim Kingdon, 19-May-2023.) |
inf | ||
18-May-2023 | xrminrecl 11035 | The minimum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 18-May-2023.) |
inf inf | ||
18-May-2023 | ralnex2 2569 | Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 18-May-2023.) |
17-May-2023 | bdtrilem 11003 | Lemma for bdtri 11004. (Contributed by Steven Nguyen and Jim Kingdon, 17-May-2023.) |
15-May-2023 | xrbdtri 11038 | Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.) |
inf inf inf | ||
15-May-2023 | bdtri 11004 | Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.) |
inf inf inf | ||
15-May-2023 | minabs 11000 | The minimum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 15-May-2023.) |
inf | ||
11-May-2023 | xrmaxadd 11023 | Distributing addition over maximum. (Contributed by Jim Kingdon, 11-May-2023.) |
11-May-2023 | xrmaxaddlem 11022 | Lemma for xrmaxadd 11023. The case where is real. (Contributed by Jim Kingdon, 11-May-2023.) |
10-May-2023 | xrminadd 11037 | Distributing addition over minimum. (Contributed by Jim Kingdon, 10-May-2023.) |
inf inf | ||
10-May-2023 | xrmaxlesup 11021 | Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 10-May-2023.) |
10-May-2023 | xrltmaxsup 11019 | The maximum as a least upper bound. (Contributed by Jim Kingdon, 10-May-2023.) |
9-May-2023 | bdxmet 12659 | The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.) |
inf | ||
9-May-2023 | bdmetval 12658 | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.) |
inf inf | ||
7-May-2023 | setsmstsetg 12639 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.) |
sSet TopSet TopSet | ||
6-May-2023 | dsslid 12108 | Slot property of . (Contributed by Jim Kingdon, 6-May-2023.) |
Slot | ||
5-May-2023 | mopnrel 12599 | The class of open sets of a metric space is a relation. (Contributed by Jim Kingdon, 5-May-2023.) |
5-May-2023 | fsumsersdc 11157 | Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Jim Kingdon, 5-May-2023.) |
DECID | ||
4-May-2023 | blex 12545 | A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.) |
4-May-2023 | summodc 11145 | A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.) |
♯ ♯ DECID | ||
4-May-2023 | summodclem2 11144 | Lemma for summodc 11145. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.) |
♯ DECID | ||
4-May-2023 | xrminrpcl 11036 | The minimum of two positive reals is a positive real. (Contributed by Jim Kingdon, 4-May-2023.) |
inf | ||
4-May-2023 | xrlemininf 11033 | Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 4-May-2023.) |
inf | ||
3-May-2023 | xrltmininf 11032 | Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 3-May-2023.) |
inf | ||
3-May-2023 | xrmineqinf 11031 | The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) (Revised by Jim Kingdon, 3-May-2023.) |
inf | ||
3-May-2023 | xrmin2inf 11030 | The minimum of two extended reals is less than or equal to the second. (Contributed by Jim Kingdon, 3-May-2023.) |
inf | ||
3-May-2023 | xrmin1inf 11029 | The minimum of two extended reals is less than or equal to the first. (Contributed by Jim Kingdon, 3-May-2023.) |
inf | ||
3-May-2023 | xrmincl 11028 | The minumum of two extended reals is an extended real. (Contributed by Jim Kingdon, 3-May-2023.) |
inf | ||
2-May-2023 | xrminmax 11027 | Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 2-May-2023.) |
inf | ||
2-May-2023 | xrnegcon1d 11026 | Contraposition law for extended real unary minus. (Contributed by Jim Kingdon, 2-May-2023.) |
2-May-2023 | infxrnegsupex 11025 | The infimum of a set of extended reals is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 2-May-2023.) |
inf | ||
2-May-2023 | xrnegiso 11024 | Negation is an order anti-isomorphism of the extended reals, which is its own inverse. (Contributed by Jim Kingdon, 2-May-2023.) |
30-Apr-2023 | xrmaxltsup 11020 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 30-Apr-2023.) |
30-Apr-2023 | xrmaxrecl 11017 | The maximum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 30-Apr-2023.) |
30-Apr-2023 | xrmax2sup 11016 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.) |
30-Apr-2023 | xrmax1sup 11015 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.) |
29-Apr-2023 | xrmaxcl 11014 | The maximum of two extended reals is an extended real. (Contributed by Jim Kingdon, 29-Apr-2023.) |
29-Apr-2023 | xrmaxiflemval 11012 | Lemma for xrmaxif 11013. Value of the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.) |
29-Apr-2023 | xrmaxiflemcom 11011 | Lemma for xrmaxif 11013. Commutativity of an expression which we will later show to be the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.) |
29-Apr-2023 | xrmaxiflemcl 11007 | Lemma for xrmaxif 11013. Closure. (Contributed by Jim Kingdon, 29-Apr-2023.) |
29-Apr-2023 | sbco2v 1919 | Version of sbco2 1936 with disjoint variable conditions. (Contributed by Wolf Lammen, 29-Apr-2023.) |
28-Apr-2023 | xrmaxiflemlub 11010 | Lemma for xrmaxif 11013. A least upper bound for . (Contributed by Jim Kingdon, 28-Apr-2023.) |
26-Apr-2023 | xrmaxif 11013 | Maximum of two extended reals in terms of expressions. (Contributed by Jim Kingdon, 26-Apr-2023.) |
26-Apr-2023 | xrmaxiflemab 11009 | Lemma for xrmaxif 11013. A variation of xrmaxleim 11006- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 26-Apr-2023.) |
26-Apr-2023 | xrmaxifle 11008 | An upper bound for in the extended reals. (Contributed by Jim Kingdon, 26-Apr-2023.) |
25-Apr-2023 | xrmaxleim 11006 | Value of maximum when we know which extended real is larger. (Contributed by Jim Kingdon, 25-Apr-2023.) |
25-Apr-2023 | rpmincl 11002 | The minumum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 25-Apr-2023.) |
inf | ||
25-Apr-2023 | mincl 10995 | The minumum of two real numbers is a real number. (Contributed by Jim Kingdon, 25-Apr-2023.) |
inf | ||
24-Apr-2023 | psmetrel 12480 | The class of pseudometrics is a relation. (Contributed by Jim Kingdon, 24-Apr-2023.) |
PsMet | ||
23-Apr-2023 | bcval5 10502 | Write out the top and bottom parts of the binomial coefficient explicitly. In this form, it is valid even for , although it is no longer valid for nonpositive . (Contributed by Mario Carneiro, 22-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.) |
23-Apr-2023 | ser3le 10284 | Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Jim Kingdon, 23-Apr-2023.) |
23-Apr-2023 | seq3z 10277 | If the operation has an absorbing element (a.k.a. zero element), then any sequence containing a evaluates to . (Contributed by Mario Carneiro, 27-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.) |
23-Apr-2023 | seq3caopr 10249 | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 23-Apr-2023.) |
23-Apr-2023 | seq3caopr2 10248 | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.) |
22-Apr-2023 | ser3sub 10272 | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.) |
22-Apr-2023 | seq3caopr3 10247 | Lemma for seq3caopr2 10248. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by Jim Kingdon, 22-Apr-2023.) |
..^ | ||
22-Apr-2023 | ser3mono 10244 | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.) |
21-Apr-2023 | metrtri 12535 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 21-Apr-2023.) |
21-Apr-2023 | sqxpeq0 4957 | A Cartesian square is empty iff its member is empty. (Contributed by Jim Kingdon, 21-Apr-2023.) |
20-Apr-2023 | xmetrel 12501 | The class of extended metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.) |
20-Apr-2023 | metrel 12500 | The class of metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.) |
19-Apr-2023 | psmetge0 12489 | The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon, 19-Apr-2023.) |
PsMet | ||
18-Apr-2023 | xleaddadd 9663 | Cancelling a factor of two in (expressed as addition rather than as a factor to avoid extended real multiplication). (Contributed by Jim Kingdon, 18-Apr-2023.) |
17-Apr-2023 | xposdif 9658 | Extended real version of posdif 8210. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.) |
17-Apr-2023 | nmnfgt 9594 | An extended real is greater than minus infinite iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.) |
17-Apr-2023 | npnflt 9591 | An extended real is less than plus infinity iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.) |
16-Apr-2023 | xltadd1 9652 | Extended real version of ltadd1 8184. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.) |
13-Apr-2023 | xrmnfdc 9619 | An extended real is or is not minus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.) |
DECID | ||
13-Apr-2023 | xrpnfdc 9618 | An extended real is or is not plus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.) |
DECID | ||
11-Apr-2023 | dmxpid 4755 | The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.) |
9-Apr-2023 | isumz 11151 | Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 9-Apr-2023.) |
DECID | ||
9-Apr-2023 | summodclem2a 11143 | Lemma for summodc 11145. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.) |
DECID ♯ ♯ | ||
9-Apr-2023 | summodclem3 11142 | Lemma for summodc 11145. (Contributed by Mario Carneiro, 29-Mar-2014.) (Revised by Jim Kingdon, 9-Apr-2023.) |
9-Apr-2023 | sumrbdc 11140 | Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Jim Kingdon, 9-Apr-2023.) |
DECID DECID | ||
9-Apr-2023 | seq3coll 10578 | The function contains a sparse set of nonzero values to be summed. The function is an order isomorphism from the set of nonzero values of to a 1-based finite sequence, and collects these nonzero values together. Under these conditions, the sum over the values in yields the same result as the sum over the original set . (Contributed by Mario Carneiro, 2-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.) |
♯ ♯ ♯ ♯ | ||
8-Apr-2023 | zsumdc 11146 | Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) (Revised by Jim Kingdon, 8-Apr-2023.) |
DECID | ||
8-Apr-2023 | sumrbdclem 11138 | Lemma for sumrbdc 11140. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 8-Apr-2023.) |
DECID | ||
8-Apr-2023 | isermulc2 11102 | Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.) |
8-Apr-2023 | seq3id 10274 | Discarding the first few terms of a sequence that starts with all zeroes (or any element which is a left-identity for ) has no effect on its sum. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 8-Apr-2023.) |
8-Apr-2023 | seq3id3 10273 | A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a -idempotent sums (or "'s") to that element. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Jim Kingdon, 8-Apr-2023.) |
7-Apr-2023 | seq3shft2 10239 | Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.) |
7-Apr-2023 | seq3feq 10238 | Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.) |
7-Apr-2023 | r19.2m 3444 | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1617). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) (Revised by Jim Kingdon, 7-Apr-2023.) |
6-Apr-2023 | lmtopcnp 12408 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) (Revised by Jim Kingdon, 6-Apr-2023.) |
6-Apr-2023 | cnptoprest2 12398 | Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 6-Apr-2023.) |
↾t | ||
5-Apr-2023 | cnptoprest 12397 | Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 5-Apr-2023.) |
↾t | ||
4-Apr-2023 | exmidmp 7024 | Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.) |
EXMID Markov | ||
2-Apr-2023 | sup3exmid 8708 | If any inhabited set of real numbers bounded from above has a supremum, excluded middle follows. (Contributed by Jim Kingdon, 2-Apr-2023.) |
DECID | ||
31-Mar-2023 | cnptopresti 12396 | One direction of cnptoprest 12397 under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 31-Mar-2023.) |
TopOn ↾t | ||
30-Mar-2023 | cncnp2m 12389 | A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Jim Kingdon, 30-Mar-2023.) |
29-Mar-2023 | exmidlpo 7008 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
EXMID Omni | ||
28-Mar-2023 | icnpimaex 12369 | Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) (Revised by Jim Kingdon, 28-Mar-2023.) |
TopOn TopOn | ||
28-Mar-2023 | cnpf2 12365 | A continuous function at point is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.) |
TopOn TopOn | ||
28-Mar-2023 | cnprcl2k 12364 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.) |
TopOn | ||
27-Mar-2023 | mptrcl 5496 | Reverse closure for a mapping: If the function value of a mapping has a member, the argument belongs to the base class of the mapping. (Contributed by AV, 4-Apr-2020.) (Revised by Jim Kingdon, 27-Mar-2023.) |
25-Mar-2023 | lmreltop 12351 | The topological space convergence relation is a relation. (Contributed by Jim Kingdon, 25-Mar-2023.) |
25-Mar-2023 | fodjumkv 7027 | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ | ||
25-Mar-2023 | fodjumkvlemres 7026 | Lemma for fodjumkv 7027. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ inl | ||
25-Mar-2023 | fodju0 7012 | Lemma for fodjuomni 7014 and fodjumkv 7027. A condition which shows that is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
25-Mar-2023 | fodjum 7011 | Lemma for fodjuomni 7014 and fodjumkv 7027. A condition which shows that is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
25-Mar-2023 | fodjuf 7010 | Lemma for fodjuomni 7014 and fodjumkv 7027. Domain and range of . (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
23-Mar-2023 | restrcl 12325 | Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Jim Kingdon, 23-Mar-2023.) |
↾t | ||
22-Mar-2023 | neipsm 12312 | A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.) (Revised by Jim Kingdon, 22-Mar-2023.) |
19-Mar-2023 | mkvprop 7025 | Markov's Principle expressed in terms of propositions (or more precisely, the case is Markov's Principle). (Contributed by Jim Kingdon, 19-Mar-2023.) |
Markov DECID | ||
18-Mar-2023 | omnimkv 7023 | An omniscient set is Markov. In particular, the case where is means that the Limited Principle of Omniscience (LPO) implies Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.) |
Omni Markov | ||
18-Mar-2023 | ismkvmap 7021 | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
18-Mar-2023 | ismkv 7020 | The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
18-Mar-2023 | df-markov 7019 |
A Markov set is one where if a predicate (here represented by a function
) on that set
does not hold (where hold means is equal to )
for all elements, then there exists an element where it fails (is equal
to ). Generalization of definition 2.5 of [Pierik], p. 9.
In particular, Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
17-Mar-2023 | finct 6994 | A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.) |
⊔ | ||
16-Mar-2023 | ctmlemr 6986 | Lemma for ctm 6987. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.) |
⊔ | ||
15-Mar-2023 | caseinl 6969 | Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.) |
case inl | ||
13-Mar-2023 | enumct 6993 | A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen], p. 73 (except that our definition of countable does not require the set to be inhabited). "Finitely enumerable" is defined as per Definition 8.1.4 of [AczelRathjen], p. 71 and "countable" is defined as ⊔ per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
13-Mar-2023 | enumctlemm 6992 | Lemma for enumct 6993. The case where is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.) |
13-Mar-2023 | ctm 6987 | Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
13-Mar-2023 | 0ct 6985 | The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
13-Mar-2023 | ctex 6640 | A class dominated by is a set. See also ctfoex 6996 which says that a countable class is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.) |
12-Mar-2023 | cls0 12291 | The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.) |
12-Mar-2023 | algrp1 11716 | The value of the algorithm iterator at . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.) |
12-Mar-2023 | ialgr0 11714 | The value of the algorithm iterator at is the initial state . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.) |
11-Mar-2023 | ntreq0 12290 | Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.) |
11-Mar-2023 | clstop 12285 | The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007.) (Proof shortened by Jim Kingdon, 11-Mar-2023.) |
11-Mar-2023 | ntrss 12277 | Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.) |
10-Mar-2023 | iuncld 12273 | A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) (Revised by Jim Kingdon, 10-Mar-2023.) |
5-Mar-2023 | 2basgeng 12240 | Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon, 5-Mar-2023.) |
5-Mar-2023 | exmidsssn 4120 | Excluded middle is equivalent to the biconditionalized version of sssnr 3675 for sets. (Contributed by Jim Kingdon, 5-Mar-2023.) |
EXMID | ||
5-Mar-2023 | exmidn0m 4119 | Excluded middle is equivalent to any set being empty or inhabited. (Contributed by Jim Kingdon, 5-Mar-2023.) |
EXMID | ||
4-Mar-2023 | eltg3 12215 | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.) |
4-Mar-2023 | tgvalex 12208 | The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.) |
4-Mar-2023 | biadanii 602 | Inference associated with biadani 601. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.) |
4-Mar-2023 | biadani 601 | An implication implies to the equivalence of some implied equivalence and some other equivalence involving a conjunction. (Contributed by BJ, 4-Mar-2023.) |
16-Feb-2023 | ixp0 6618 | The infinite Cartesian product of a family with an empty member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim Kingdon, 16-Feb-2023.) |
16-Feb-2023 | ixpm 6617 | If an infinite Cartesian product of a family is inhabited, every is inhabited. (Contributed by Mario Carneiro, 22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.) |
16-Feb-2023 | exmidundifim 4125 | Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4124 with an implication rather than a biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.) |
EXMID | ||
15-Feb-2023 | ixpintm 6612 | The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.) |
15-Feb-2023 | ixpiinm 6611 | The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.) |
15-Feb-2023 | ixpexgg 6609 | The existence of an infinite Cartesian product. is normally a free-variable parameter in . Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Jim Kingdon, 15-Feb-2023.) |
15-Feb-2023 | nfixpxy 6604 | Bound-variable hypothesis builder for indexed Cartesian product. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon, 15-Feb-2023.) |
13-Feb-2023 | topnpropgd 12123 | The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon, 13-Feb-2023.) |
TopSet TopSet | ||
12-Feb-2023 | slotex 11975 | Existence of slot value. A corollary of slotslfn 11974. (Contributed by Jim Kingdon, 12-Feb-2023.) |
Slot | ||
11-Feb-2023 | topnvalg 12121 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.) |
TopSet ↾t | ||
10-Feb-2023 | slotslfn 11974 | A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.) |
Slot | ||
9-Feb-2023 | pleslid 12105 | Slot property of . (Contributed by Jim Kingdon, 9-Feb-2023.) |
Slot | ||
9-Feb-2023 | topgrptsetd 12102 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
TopSet TopSet | ||
9-Feb-2023 | topgrpplusgd 12101 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
TopSet | ||
9-Feb-2023 | topgrpbasd 12100 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
TopSet | ||
9-Feb-2023 | topgrpstrd 12099 | A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
TopSet Struct | ||
9-Feb-2023 | tsetslid 12098 | Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.) |
TopSet Slot TopSet TopSet | ||
8-Feb-2023 | ipsipd 12095 | The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.) |
Scalar | ||
8-Feb-2023 | ipsvscad 12094 | The scalar product operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.) |
Scalar | ||
8-Feb-2023 | ipsscad 12093 | The set of scalars of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.) |
Scalar Scalar | ||
7-Feb-2023 | ipsmulrd 12092 | The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar | ||
7-Feb-2023 | ipsaddgd 12091 | The additive operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar | ||
7-Feb-2023 | ipsbased 12090 | The base set of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar | ||
7-Feb-2023 | ipsstrd 12089 | A constructed inner product space is a structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar Struct | ||
7-Feb-2023 | ipslid 12088 | Slot property of . (Contributed by Jim Kingdon, 7-Feb-2023.) |
Slot | ||
7-Feb-2023 | lmodvscad 12085 | The scalar product operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar | ||
6-Feb-2023 | lmodscad 12084 | The set of scalars of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.) |
Scalar Scalar | ||
6-Feb-2023 | lmodplusgd 12083 | The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.) |
Scalar | ||
6-Feb-2023 | lmodbased 12082 | The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.) |
Scalar | ||
5-Feb-2023 | lmodstrd 12081 | A constructed left module or left vector space is a structure. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Jim Kingdon, 5-Feb-2023.) |
Scalar Struct | ||
5-Feb-2023 | vscaslid 12080 | Slot property of . (Contributed by Jim Kingdon, 5-Feb-2023.) |
Slot | ||
5-Feb-2023 | scaslid 12077 | Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.) |
Scalar Slot Scalar Scalar | ||
5-Feb-2023 | srngplusgd 12072 | The addition operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.) |
5-Feb-2023 | srngbased 12071 | The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.) |
5-Feb-2023 | srngstrd 12070 | A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.) |
Struct | ||
5-Feb-2023 | opelstrsl 12044 | The slot of a structure which contains an ordered pair for that slot. (Contributed by Jim Kingdon, 5-Feb-2023.) |
Slot Struct | ||
4-Feb-2023 | starvslid 12069 | Slot property of . (Contributed by Jim Kingdon, 4-Feb-2023.) |
Slot | ||
3-Feb-2023 | rngbaseg 12064 | The base set of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.) |
3-Feb-2023 | rngstrg 12063 | A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.) |
Struct | ||
3-Feb-2023 | mulrslid 12060 | Slot property of . (Contributed by Jim Kingdon, 3-Feb-2023.) |
Slot | ||
3-Feb-2023 | plusgslid 12043 | Slot property of . (Contributed by Jim Kingdon, 3-Feb-2023.) |
Slot | ||
2-Feb-2023 | 2strop1g 12053 | The other slot of a constructed two-slot structure. Version of 2stropg 12050 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
Slot | ||
2-Feb-2023 | 2strbas1g 12052 | The base set of a constructed two-slot structure. Version of 2strbasg 12049 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
2-Feb-2023 | 2strstr1g 12051 | A constructed two-slot structure. Version of 2strstrg 12048 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
Struct | ||
31-Jan-2023 | baseslid 12004 | The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.) |
Slot | ||
31-Jan-2023 | strsl0 11996 | All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.) |
Slot | ||
31-Jan-2023 | strslss 11995 | Propagate component extraction to a structure from a subset structure . (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Jim Kingdon, 31-Jan-2023.) |
Slot | ||
31-Jan-2023 | strslssd 11994 | Deduction version of strslss 11995. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 31-Jan-2023.) |
Slot | ||
30-Jan-2023 | strslfv3 11993 | Variant on strslfv 11992 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Struct Slot | ||
30-Jan-2023 | strslfv 11992 | Extract a structure component (such as the base set) from a structure with a component extractor (such as the base set extractor df-base 11954). By virtue of ndxslid 11973, this can be done without having to refer to the hard-coded numeric index of . (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Struct Slot | ||
30-Jan-2023 | strslfv2 11991 | A variation on strslfv 11992 to avoid asserting that itself is a function, which involves sethood of all the ordered pair components of . (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot | ||
30-Jan-2023 | strslfv2d 11990 | Deduction version of strslfv 11992. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot | ||
30-Jan-2023 | strslfvd 11989 | Deduction version of strslfv 11992. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot | ||
30-Jan-2023 | strsetsid 11981 | Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot Struct sSet | ||
30-Jan-2023 | funresdfunsndc 6395 | Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself, where equality is decidable. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon, 30-Jan-2023.) |
DECID | ||
29-Jan-2023 | ndxslid 11973 | A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 11992. (Contributed by Jim Kingdon, 29-Jan-2023.) |
Slot Slot | ||
29-Jan-2023 | fnsnsplitdc 6394 | Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 29-Jan-2023.) |
DECID | ||
28-Jan-2023 | 2stropg 12050 | The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
Slot | ||
28-Jan-2023 | 2strbasg 12049 | The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
Slot | ||
28-Jan-2023 | 2strstrg 12048 | A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
Slot Struct | ||
28-Jan-2023 | 1strstrg 12046 | A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Revised by Jim Kingdon, 28-Jan-2023.) |
Struct | ||
27-Jan-2023 | strle2g 12039 | Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
Struct | ||
27-Jan-2023 | strle1g 12038 | Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
Struct | ||
27-Jan-2023 | strleund 12036 | Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
Struct Struct Struct | ||
26-Jan-2023 | ressid2 12007 | General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 26-Jan-2023.) |
↾s | ||
24-Jan-2023 | setsslnid 11999 | Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.) |
Slot sSet | ||
24-Jan-2023 | setsslid 11998 | Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.) |
Slot sSet | ||
22-Jan-2023 | setsabsd 11987 | Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.) |
sSet sSet sSet | ||
22-Jan-2023 | setsresg 11986 | The structure replacement function does not affect the value of away from . (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.) |
sSet | ||
22-Jan-2023 | setsex 11980 | Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.) |
sSet | ||
22-Jan-2023 | 2zsupmax 10990 | Two ways to express the maximum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 22-Jan-2023.) |
22-Jan-2023 | elpwpwel 4391 | A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.) |
21-Jan-2023 | funresdfunsnss 5616 | Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in a subset of the function itself. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon, 21-Jan-2023.) |
20-Jan-2023 | setsvala 11979 | Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.) |
sSet | ||
20-Jan-2023 | fnsnsplitss 5612 | Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 20-Jan-2023.) |
19-Jan-2023 | strfvssn 11970 | A structure component extractor produces a value which is contained in a set dependent on , but not . This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
19-Jan-2023 | strnfvn 11969 |
Value of a structure component extractor . Normally, is a
defined constant symbol such as (df-base 11954) and is a
fixed integer such as . is a
structure, i.e. a specific
member of a class of structures.
Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 11992. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.) |
Slot | ||
19-Jan-2023 | strnfvnd 11968 | Deduction version of strnfvn 11969. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
18-Jan-2023 | isstructr 11963 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
18-Jan-2023 | isstructim 11962 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
18-Jan-2023 | isstruct2r 11959 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
18-Jan-2023 | isstruct2im 11958 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
18-Jan-2023 | sbiev 1765 | Conversion of implicit substitution to explicit substitution. Version of sbie 1764 with a disjoint variable condition. (Contributed by Wolf Lammen, 18-Jan-2023.) |
16-Jan-2023 | toponsspwpwg 12178 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) (Revised by Jim Kingdon, 16-Jan-2023.) |
TopOn | ||
14-Jan-2023 | istopfin 12156 | Express the predicate " is a topology" using nonempty finite intersections instead of binary intersections as in istopg 12155. It is not clear we can prove the converse without adding additional conditions. (Contributed by NM, 19-Jul-2006.) (Revised by Jim Kingdon, 14-Jan-2023.) |
14-Jan-2023 | fiintim 6810 |
If a class is closed under pairwise intersections, then it is closed
under nonempty finite intersections. The converse would appear to
require an additional condition, such as and not being
equal, or
having decidable equality.
This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.) |
9-Jan-2023 | divccncfap 12735 | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.) |
# | ||
7-Jan-2023 | eap1 11481 | is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.) |
# | ||
7-Jan-2023 | eap0 11479 | is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.) |
# | ||
7-Jan-2023 | egt2lt3 11475 | Euler's constant = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Jim Kingdon, 7-Jan-2023.) |
6-Jan-2023 | eirr 11474 | is not rational. In the absence of excluded middle, we can distinguish between this and saying that is irrational in the sense of being apart from any rational number, which is eirrap 11473. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.) |
6-Jan-2023 | eirrap 11473 | is irrational. That is, for any rational number, is apart from it. In the absence of excluded middle, we can distinguish between this and saying that is not rational, which is eirr 11474. (Contributed by Jim Kingdon, 6-Jan-2023.) |
# | ||
6-Jan-2023 | btwnapz 9174 | A number between an integer and its successor is apart from any integer. (Contributed by Jim Kingdon, 6-Jan-2023.) |
# | ||
6-Jan-2023 | apmul2 8542 | Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 6-Jan-2023.) |
# # # | ||
1-Jan-2023 | nnap0i 8744 | A positive integer is apart from zero (inference version). (Contributed by Jim Kingdon, 1-Jan-2023.) |
# | ||
26-Dec-2022 | apdivmuld 8566 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 26-Dec-2022.) |
# # # | ||
25-Dec-2022 | tanaddaplem 11434 | A useful intermediate step in tanaddap 11435 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) (Revised by Jim Kingdon, 25-Dec-2022.) |
# # # # | ||
25-Dec-2022 | subap0 8398 | Two numbers being apart is equivalent to their difference being apart from zero. (Contributed by Jim Kingdon, 25-Dec-2022.) |
# # | ||
23-Dec-2022 | sqrt2irr0 11831 | The square root of 2 is not rational. (Contributed by AV, 23-Dec-2022.) |
22-Dec-2022 | tanval3ap 11410 | Express the tangent function directly in terms of . (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
22-Dec-2022 | tanval2ap 11409 | Express the tangent function directly in terms of . (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
22-Dec-2022 | tanclapd 11408 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
21-Dec-2022 | tanclap 11405 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.) |
# | ||
21-Dec-2022 | tanvalap 11404 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.) |
# | ||
20-Dec-2022 | reef11 11395 | The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Jim Kingdon, 20-Dec-2022.) |
20-Dec-2022 | efler 11394 | The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 20-Dec-2022.) |
20-Dec-2022 | efltim 11393 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 20-Dec-2022.) |
20-Dec-2022 | eqord1 8238 | A strictly increasing real function on a subset of is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by Jim Kingdon, 20-Dec-2022.) |
14-Dec-2022 | iserabs 11237 | Generalized triangle inequality: the absolute value of an infinite sum is less than or equal to the sum of absolute values. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Jim Kingdon, 14-Dec-2022.) |
12-Dec-2022 | efap0 11372 | The exponential of a complex number is apart from zero. (Contributed by Jim Kingdon, 12-Dec-2022.) |
# | ||
8-Dec-2022 | efcllem 11354 | Lemma for efcl 11359. The series that defines the exponential function converges. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 8-Dec-2022.) |
8-Dec-2022 | efcllemp 11353 | Lemma for efcl 11359. The series that defines the exponential function converges. The ratio test cvgratgt0 11295 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 8-Dec-2022.) |
8-Dec-2022 | eftvalcn 11352 | The value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 8-Dec-2022.) |
8-Dec-2022 | mertensabs 11299 | Mertens' theorem. If is an absolutely convergent series and is convergent, then (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 8-Dec-2022.) |
3-Dec-2022 | mertenslemub 11296 | Lemma for mertensabs 11299. An upper bound for . (Contributed by Jim Kingdon, 3-Dec-2022.) |
2-Dec-2022 | mertenslemi1 11297 | Lemma for mertensabs 11299. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.) |
2-Dec-2022 | fsum3cvg3 11158 | A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.) |
DECID | ||
2-Dec-2022 | fsum3cvg2 11156 | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.) |
DECID | ||
24-Nov-2022 | cvgratnnlembern 11285 | Lemma for cvgratnn 11293. Upper bound for a geometric progression of positive ratio less than one. (Contributed by Jim Kingdon, 24-Nov-2022.) |
23-Nov-2022 | cvgratnnlemfm 11291 | Lemma for cvgratnn 11293. (Contributed by Jim Kingdon, 23-Nov-2022.) |
23-Nov-2022 | cvgratnnlemsumlt 11290 | Lemma for cvgratnn 11293. (Contributed by Jim Kingdon, 23-Nov-2022.) |
21-Nov-2022 | cvgratnnlemrate 11292 | Lemma for cvgratnn 11293. (Contributed by Jim Kingdon, 21-Nov-2022.) |
21-Nov-2022 | cvgratnnlemabsle 11289 | Lemma for cvgratnn 11293. (Contributed by Jim Kingdon, 21-Nov-2022.) |
21-Nov-2022 | cvgratnnlemseq 11288 | Lemma for cvgratnn 11293. (Contributed by Jim Kingdon, 21-Nov-2022.) |
15-Nov-2022 | cvgratnnlemmn 11287 | Lemma for cvgratnn 11293. (Contributed by Jim Kingdon, 15-Nov-2022.) |
15-Nov-2022 | cvgratnnlemnexp 11286 | Lemma for cvgratnn 11293. (Contributed by Jim Kingdon, 15-Nov-2022.) |
12-Nov-2022 | cvgratnn 11293 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms, then the infinite sum of the terms of converges to a complex number. Although this theorem is similar to cvgratz 11294 and cvgratgt0 11295, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 11112 is sensitive to how a sequence is indexed. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 12-Nov-2022.) |
12-Nov-2022 | fsum3cvg 11139 | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 12-Nov-2022.) |
DECID | ||
12-Nov-2022 | seq3id2 10275 | The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for ) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 12-Nov-2022.) |
11-Nov-2022 | cvgratgt0 11295 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms beyond some index , then the infinite sum of the terms of converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.) |
11-Nov-2022 | cvgratz 11294 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms, then the infinite sum of the terms of converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.) |
4-Nov-2022 | seq3val 10224 | Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 10227, seq3-1 10226 and seq3p1 10228, as further development can be done in terms of those. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 4-Nov-2022.) |
frec | ||
4-Nov-2022 | df-seqfrec 10212 |
Define a general-purpose operation that builds a recursive sequence
(i.e., a function on an upper integer set such as or )
whose value at an index is a function of its previous value and the
value of an input sequence at that index. This definition is
complicated, but fortunately it is not intended to be used directly.
Instead, the only purpose of this definition is to provide us with an
object that has the properties expressed by seqf 10227, seq3-1 10226 and
seq3p1 10228. Typically, those are the main theorems
that would be used in
practice.
The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation , an input sequence with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence with values 1, 3/2, 7/4, 15/8,.., so that , 3/2, etc. In other words, transforms a sequence into an infinite series. means "the sum of F(n) from n = M to infinity is 2." Since limits are unique (climuni 11055), by climdm 11057 the "sum of F(n) from n = 1 to infinity" can be expressed as (provided the sequence converges) and evaluates to 2 in this example. Internally, the frec function generates as its values a set of ordered pairs starting at , with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by NM, 18-Apr-2005.) (Revised by Jim Kingdon, 4-Nov-2022.) |
frec | ||
3-Nov-2022 | seq3f1o 10270 | Rearrange a sum via an arbitrary bijection on . (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 3-Nov-2022.) |
3-Nov-2022 | seq3m1 10234 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 3-Nov-2022.) |
29-Oct-2022 | absgtap 11272 | Greater-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
29-Oct-2022 | absltap 11271 | Less-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
29-Oct-2022 | 1ap2 8920 | 1 is apart from 2. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
28-Oct-2022 | expcnv 11266 | A sequence of powers of a complex number with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 28-Oct-2022.) |
28-Oct-2022 | expcnvre 11265 | A sequence of powers of a nonnegative real number less than one converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.) |
27-Oct-2022 | ennnfone 11927 | A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that is countable (that's the part, as seen in theorems like ctm 6987), infinite (that's the part about being able to find an element of distinct from any mapping of a natural number via ), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
27-Oct-2022 | ennnfonelemim 11926 | Lemma for ennnfone 11927. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
27-Oct-2022 | ennnfonelemr 11925 | Lemma for ennnfone 11927. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
27-Oct-2022 | ennnfonelemnn0 11924 | Lemma for ennnfone 11927. A version of ennnfonelemen 11923 expressed in terms of instead of . (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID frec | ||
24-Oct-2022 | pwm1geoserap1 11270 | The n-th power of a number decreased by 1 expressed by the finite geometric series ... . (Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# | ||
24-Oct-2022 | geoserap 11269 | The value of the finite geometric series ... . This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# | ||
24-Oct-2022 | geosergap 11268 | The value of the finite geometric series ... . (Contributed by Mario Carneiro, 2-May-2016.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# ..^ | ||
23-Oct-2022 | expcnvap0 11264 | A sequence of powers of a complex number with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 23-Oct-2022.) |
# | ||
22-Oct-2022 | divcnv 11259 | The sequence of reciprocals of positive integers, multiplied by the factor , converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Jim Kingdon, 22-Oct-2022.) |
22-Oct-2022 | impcomd 253 | Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.) |
21-Oct-2022 | isumsplit 11253 | Split off the first terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.) |
21-Oct-2022 | seq3split 10245 | Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) (Revised by Jim Kingdon, 21-Oct-2022.) |
20-Oct-2022 | fidcenumlemrk 6835 | Lemma for fidcenum 6837. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
20-Oct-2022 | fidcenumlemrks 6834 | Lemma for fidcenum 6837. Induction step for fidcenumlemrk 6835. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenum 6837 | A set is finite if and only if it has decidable equality and is finitely enumerable. Proposition 8.1.11 of [AczelRathjen], p. 72. The definition of "finitely enumerable" as is Definition 8.1.4 of [AczelRathjen], p. 71. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenumlemr 6836 | Lemma for fidcenum 6837. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenumlemim 6833 | Lemma for fidcenum 6837. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
17-Oct-2022 | iser3shft 11108 | Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Jim Kingdon, 17-Oct-2022.) |
17-Oct-2022 | seq3shft 10603 | Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 17-Oct-2022.) |
16-Oct-2022 | resqrexlemf1 10773 | Lemma for resqrex 10791. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlemf 10772 | Lemma for resqrex 10791. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlemp1rp 10771 | Lemma for resqrex 10791. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10227 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlem1arp 10770 | Lemma for resqrex 10791. is a positive real (expressed in a way that will help apply seqf 10227 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
15-Oct-2022 | inffz 13227 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
inf | ||
15-Oct-2022 | supfz 13226 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
12-Oct-2022 | fsumlessfi 11222 | A shorter sum of nonnegative terms is no greater than a longer one. (Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon, 12-Oct-2022.) |
12-Oct-2022 | modfsummodlemstep 11219 | Induction step for modfsummod 11220. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.) |
10-Oct-2022 | fsum3 11149 | The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | fsumgcl 11148 | Closure for a function used to describe a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | seq3distr 10279 | The distributive property for series. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | seq3homo 10276 | Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 10-Oct-2022.) |
8-Oct-2022 | fsum2dlemstep 11196 | Lemma for fsum2d 11197- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.) |
7-Oct-2022 | iunfidisj 6827 | The finite union of disjoint finite sets is finite. Note that depends on , i.e. can be thought of as . (Contributed by NM, 23-Mar-2006.) (Revised by Jim Kingdon, 7-Oct-2022.) |
Disj | ||
7-Oct-2022 | disjnims 3916 | If a collection for is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by Jim Kingdon, 7-Oct-2022.) |
Disj | ||
6-Oct-2022 | disjnim 3915 | If a collection for is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Jim Kingdon, 6-Oct-2022.) |
Disj | ||
5-Oct-2022 | dcun 3468 | The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) |
DECID DECID DECID | ||
4-Oct-2022 | ser3add 10271 | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 4-Oct-2022.) |
3-Oct-2022 | seq3-1 10226 | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 3-Oct-2022.) |
3-Oct-2022 | brrelex12i 4576 | Two classes that are related by a binary relation are sets. (An artifact of our ordered pair definition.) (Contributed by BJ, 3-Oct-2022.) |
1-Oct-2022 | fsum3ser 11159 | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 11174 and fsump1 11182, which should make our notation clear and from which, along with closure fsumcl 11162, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.) |
1-Oct-2022 | tpfidisj 6809 | A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.) |
30-Sep-2022 | exdistrv 1882 | Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1874 and 19.42v 1878. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 1902. (Contributed by BJ, 30-Sep-2022.) |
28-Sep-2022 | seq3clss 10233 | Closure property of the recursive sequence builder. (Contributed by Jim Kingdon, 28-Sep-2022.) |
27-Sep-2022 | zmaxcl 10989 | The maximum of two integers is an integer. (Contributed by Jim Kingdon, 27-Sep-2022.) |
24-Sep-2022 | isumss2 11155 | Change the index set of a sum by adding zeroes. The nonzero elements are in the contained set and the added zeroes compose the rest of the containing set which needs to be summable. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.) |
DECID DECID | ||
24-Sep-2022 | preimaf1ofi 6832 | The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.) |
24-Sep-2022 | ifmdc 3504 | If a conditional class is inhabited, then the condition is decidable. This shows that conditionals are not very useful unless one can prove the condition decidable. (Contributed by BJ, 24-Sep-2022.) |
DECID | ||
24-Sep-2022 | mpbiran2d 438 | Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.) |
23-Sep-2022 | fisumss 11154 | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.) |
DECID | ||
21-Sep-2022 | pw1dom2 13179 | The power set of dominates . Also see pwpw0ss 3726 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.) |
21-Sep-2022 | isumss 11153 | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 21-Sep-2022.) |
DECID DECID | ||
18-Sep-2022 | sumfct 11136 | A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 18-Sep-2022.) |
16-Sep-2022 | fser0const 10282 | Simplifying an expression which turns out just to be a constant zero sequence. (Contributed by Jim Kingdon, 16-Sep-2022.) |
8-Sep-2022 | zfz1isolemiso 10575 | Lemma for zfz1iso 10577. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.) |
♯ ♯ ♯ ♯ ♯ | ||
8-Sep-2022 | zfz1isolemsplit 10574 | Lemma for zfz1iso 10577. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.) |
♯ ♯ ♯ | ||
7-Sep-2022 | zfz1isolem1 10576 | Lemma for zfz1iso 10577. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.) |
♯ ♯ | ||
6-Sep-2022 | fimaxq 10566 | A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.) |
5-Sep-2022 | fimax2gtri 6788 | A finite set has a maximum under a trichotomous order. (Contributed by Jim Kingdon, 5-Sep-2022.) |
5-Sep-2022 | fimax2gtrilemstep 6787 | Lemma for fimax2gtri 6788. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.) |
5-Sep-2022 | tridc 6786 | A trichotomous order is decidable. (Contributed by Jim Kingdon, 5-Sep-2022.) |
DECID | ||
3-Sep-2022 | zfz1iso 10577 | A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.) |
♯ | ||
2-Sep-2022 | rspceeqv 2802 | Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.) |
1-Sep-2022 | ssidd 3113 | Weakening of ssid 3112. (Contributed by BJ, 1-Sep-2022.) |
31-Aug-2022 | fveqeq2 5423 | Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.) |
30-Aug-2022 | iseqf1olemfvp 10263 | Lemma for seq3f1o 10270. (Contributed by Jim Kingdon, 30-Aug-2022.) |
30-Aug-2022 | fveqeq2d 5422 | Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.) |
29-Aug-2022 | seq3f1olemqsumkj 10264 | Lemma for seq3f1o 10270. gives the same sum as in the range . (Contributed by Jim Kingdon, 29-Aug-2022.) |
..^ | ||
29-Aug-2022 | iseqf1olemqpcl 10262 | Lemma for seq3f1o 10270. A closure lemma involving and . (Contributed by Jim Kingdon, 29-Aug-2022.) |
29-Aug-2022 | iseqf1olemjpcl 10261 | Lemma for seq3f1o 10270. A closure lemma involving and . (Contributed by Jim Kingdon, 29-Aug-2022.) |
28-Aug-2022 | iseqf1olemqval 10253 | Lemma for seq3f1o 10270. Value of the function . (Contributed by Jim Kingdon, 28-Aug-2022.) |
27-Aug-2022 | iseqf1olemmo 10258 | Lemma for seq3f1o 10270. Showing that is one-to-one. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemnanb 10256 | Lemma for seq3f1o 10270. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemab 10255 | Lemma for seq3f1o 10270. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemnab 10254 | Lemma for seq3f1o 10270. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemqcl 10252 | Lemma for seq3f1o 10270. (Contributed by Jim Kingdon, 27-Aug-2022.) |
26-Aug-2022 | iseqf1olemqf 10257 | Lemma for seq3f1o 10270. Domain and codomain of . (Contributed by Jim Kingdon, 26-Aug-2022.) |
25-Aug-2022 | fzodcel 9922 | Decidability of membership in a half-open integer interval. (Contributed by Jim Kingdon, 25-Aug-2022.) |
DECID ..^ | ||
24-Aug-2022 | rspceaimv 2792 | Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.) |
22-Aug-2022 | seq3f1olemqsumk 10265 | Lemma for seq3f1o 10270. gives the same sum as in the range . (Contributed by Jim Kingdon, 22-Aug-2022.) |
..^ | ||
21-Aug-2022 | seq3f1olemqsum 10266 | Lemma for seq3f1o 10270. gives the same sum as . (Contributed by Jim Kingdon, 21-Aug-2022.) |
..^ | ||
21-Aug-2022 | iseqf1olemqk 10260 | Lemma for seq3f1o 10270. is constant for one more position than is. (Contributed by Jim Kingdon, 21-Aug-2022.) |
..^ | ||
21-Aug-2022 | iseqf1olemqf1o 10259 | Lemma for seq3f1o 10270. is a permutation of . is formed from the constant portion of , followed by the single element (at position ), followed by the rest of J (with the deleted and the elements before moved one position later to fill the gap). (Contributed by Jim Kingdon, 21-Aug-2022.) |
21-Aug-2022 | iseqf1olemklt 10251 | Lemma for seq3f1o 10270. (Contributed by Jim Kingdon, 21-Aug-2022.) |
..^ | ||
21-Aug-2022 | iseqf1olemkle 10250 | Lemma for seq3f1o 10270. (Contributed by Jim Kingdon, 21-Aug-2022.) |
..^ | ||
21-Aug-2022 | fssdm 5282 | Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, semi-deduction form. (Contributed by AV, 21-Aug-2022.) |
21-Aug-2022 | fssdmd 5281 | Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, deduction form. (Contributed by AV, 21-Aug-2022.) |
21-Aug-2022 | eqelssd 3111 | Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.) |
21-Aug-2022 | reximssdv 2534 | Derivation of a restricted existential quantification over a subset (the second hypothesis implies ), deduction form. (Contributed by AV, 21-Aug-2022.) |
21-Aug-2022 | animpimp2impd 548 | Deduction deriving nested implications from conjunctions. (Contributed by AV, 21-Aug-2022.) |
20-Aug-2022 | brimralrspcev 3982 | Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022.) |
20-Aug-2022 | brralrspcev 3981 | Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
19-Aug-2022 | seq3f1olemstep 10267 | Lemma for seq3f1o 10270. Given a permutation which is constant up to a point, supply a new one which is constant for one more position. (Contributed by Jim Kingdon, 19-Aug-2022.) |
..^ | ||
18-Aug-2022 | seq3f1olemp 10268 | Lemma for seq3f1o 10270. Existence of a constant permutation of which leads to the same sum as the permutation itself. (Contributed by Jim Kingdon, 18-Aug-2022.) |
17-Aug-2022 | seq3f1oleml 10269 | Lemma for seq3f1o 10270. This is more or less the result, but stated in terms of and without . and may differ in terms of what happens to terms after . The terms after don't matter for the value at but we need some definition given the way our theorems concerning work. (Contributed by Jim Kingdon, 17-Aug-2022.) |
17-Aug-2022 | imbrov2fvoveq 5792 | Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.) |
16-Aug-2022 | fmpttd 5568 | Version of fmptd 5567 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.) |
15-Aug-2022 | isummolemnm 11141 | Lemma for summodc 11145. (Contributed by Jim Kingdon, 15-Aug-2022.) |
14-Aug-2022 | 2fveq3 5419 | Equality theorem for nested function values. (Contributed by AV, 14-Aug-2022.) |
13-Aug-2022 | exmidsbth 13208 |
The Schroeder-Bernstein Theorem is equivalent to excluded middle. This
is Metamath 100 proof #25. The forward direction (isbth 6848) is the
proof of the Schroeder-Bernstein Theorem from the Metamath Proof
Explorer database (in which excluded middle holds), but adapted to use
EXMID as an antecedent rather than being unconditionally
true, as in
the non-intuitionist proof at
https://us.metamath.org/mpeuni/sbth.html 6848.
The reverse direction (exmidsbthr 13207) is the one which establishes that Schroeder-Bernstein implies excluded middle. This resolves the question of whether we will be able to prove Schroeder-Bernstein from our axioms in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.) |
EXMID | ||
13-Aug-2022 | fv0p1e1 8828 | Function value at with replaced by . Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
13-Aug-2022 | ovanraleqv 5791 | Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
12-Aug-2022 | stbid 817 | The equivalent of a stable proposition is stable. (Contributed by Jim Kingdon, 12-Aug-2022.) |
STAB STAB | ||
11-Aug-2022 | exmidsbthr 13207 | The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.) |
EXMID | ||
11-Aug-2022 | exmidsbthrlem 13206 | Lemma for exmidsbthr 13207. (Contributed by Jim Kingdon, 11-Aug-2022.) |
ℕ∞ EXMID | ||
10-Aug-2022 | nninfomni 13204 | ℕ∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ Omni | ||
10-Aug-2022 | nninfomnilem 13203 | Lemma for nninfomni 13204. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ ℕ∞ Omni | ||
10-Aug-2022 | nninfex 13194 | ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ | ||
10-Aug-2022 | vpwex 4098 | Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 4099 from vpwex 4098. (Revised by BJ, 10-Aug-2022.) |
9-Aug-2022 | nninfsel 13202 | is a selection function for ℕ∞. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ ℕ∞ | ||
9-Aug-2022 | nninfsellemeqinf 13201 | Lemma for nninfsel 13202. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
9-Aug-2022 | nninfsellemqall 13200 | Lemma for nninfsel 13202. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
9-Aug-2022 | nninfsellemeq 13199 | Lemma for nninfsel 13202. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
8-Aug-2022 | nninfsellemcl 13196 | Lemma for nninfself 13198. (Contributed by Jim Kingdon, 8-Aug-2022.) |
ℕ∞ | ||
8-Aug-2022 | nninfsellemdc 13195 | Lemma for nninfself 13198. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.) |
ℕ∞ DECID | ||
8-Aug-2022 | ss1oel2o 13178 | Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4116 which more directly illustrates the contrast with el2oss1o 13177. (Contributed by Jim Kingdon, 8-Aug-2022.) |
EXMID | ||
8-Aug-2022 | el2oss1o 13177 | Being an element of ordinal two implies being a subset of ordinal one. The converse is equivalent to excluded middle by ss1oel2o 13178. (Contributed by Jim Kingdon, 8-Aug-2022.) |
7-Aug-2022 | nnti 13180 | Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.) |
6-Aug-2022 | nninfself 13198 | Domain and range of the selection function for ℕ∞. (Contributed by Jim Kingdon, 6-Aug-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
6-Aug-2022 | nninfsellemsuc 13197 | Lemma for nninfself 13198. (Contributed by Jim Kingdon, 6-Aug-2022.) |
ℕ∞ | ||
4-Aug-2022 | nninfalllemn 13191 | Lemma for nninfall 13193. Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
4-Aug-2022 | nninff 13187 | An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
1-Aug-2022 | nninfall 13193 | Given a decidable predicate on ℕ∞, showing it holds for natural numbers and the point at infinity suffices to show it holds everywhere. The sense in which is a decidable predicate is that it assigns a value of either or (which can be thought of as false and true) to every element of ℕ∞. Lemma 3.5 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
1-Aug-2022 | nninfalllem1 13192 | Lemma for nninfall 13193. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
1-Aug-2022 | peano3nninf 13190 | The successor function on ℕ∞ is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
31-Jul-2022 | peano4nninf 13189 | The successor function on ℕ∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
31-Jul-2022 | 1lt2o 6332 | Ordinal one is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
31-Jul-2022 | 0lt2o 6331 | Ordinal zero is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
31-Jul-2022 | nnpredcl 4531 | The predecessor of a natural number is a natural number. This theorem is most interesting when the natural number is a successor (as seen in theorems like onsucuni2 4474) but also holds when it is by uni0 3758. (Contributed by Jim Kingdon, 31-Jul-2022.) |
31-Jul-2022 | nnsucpred 4525 | The successor of the precedessor of a nonzero natural number. (Contributed by Jim Kingdon, 31-Jul-2022.) |
30-Jul-2022 | nnsf 13188 | Domain and range of . Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
29-Jul-2022 | fodjuomnilemres 7013 | Lemma for fodjuomni 7014. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.) |
Omni ⊔ inl | ||
28-Jul-2022 | eqifdc 3501 | Expansion of an equality with a conditional operator. (Contributed by Jim Kingdon, 28-Jul-2022.) |
DECID | ||
27-Jul-2022 | fodjuomni 7014 | A condition which ensures is either inhabited or empty. Lemma 3.2 of [PradicBrown2022], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.) |
Omni ⊔ | ||
27-Jul-2022 | fodjuomnilemdc 7009 | Lemma for fodjuomni 7014. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊔ DECID inl | ||
25-Jul-2022 | djudom 6971 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊔ ⊔ | ||
23-Jul-2022 | fvoveq1 5790 | Equality theorem for nested function and operation value. Closed form of fvoveq1d 5789. (Contributed by AV, 23-Jul-2022.) |
23-Jul-2022 | fvoveq1d 5789 | Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.) |
17-Jul-2022 | inftonninf 10207 | The mapping of into ℕ∞ is the sequence of all ones. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
17-Jul-2022 | 1tonninf 10206 | The mapping of one into ℕ∞ is a sequence which is a one followed by zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
17-Jul-2022 | 0tonninf 10205 | The mapping of zero into ℕ∞ is the sequence of all zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
16-Jul-2022 | fxnn0nninf 10204 | A function from NN0* into ℕ∞. (Contributed by Jim Kingdon, 16-Jul-2022.) |
frec NN0*ℕ∞ | ||
16-Jul-2022 | fnn0nninf 10203 | A function from into ℕ∞. (Contributed by Jim Kingdon, 16-Jul-2022.) |
frec ℕ∞ | ||
15-Jul-2022 | mapdom1g 6734 | Order-preserving property of set exponentiation. (Contributed by Jim Kingdon, 15-Jul-2022.) |
14-Jul-2022 | 0nninf 13186 | The zero element of ℕ∞ (the constant sequence equal to ). (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
14-Jul-2022 | nnnninf 7016 | Elements of ℕ∞ corresponding to natural numbers. The natural number corresponds to a sequence of ones followed by zeroes. Contrast to a sequence which is all ones as seen at infnninf 7015. Remark/TODO: the theorem still holds if , that is, the antecedent could be weakened to . (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
14-Jul-2022 | infnninf 7015 | The point at infinity in ℕ∞ (the constant sequence equal to ). (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
14-Jul-2022 | df-nninf 7000 | Define the set of nonincreasing sequences in . Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as NN0* as defined at df-xnn0 9034 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used or , but the former allows us to take advantage of (df2o3 6320) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
13-Jul-2022 | uzind4i 9380 | Induction on the upper integers that start at . The first four give us the substitution instances we need, and the last two are the basis and the induction step. This is a stronger version of uzind4 9376 assuming that holds unconditionally. Notice that implies that the lower bound is an integer ( , see eluzel2 9324). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.) |
13-Jul-2022 | enomni 7004 | Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Limited Principle of Omniscience as either Omni or Omni. The former is a better match to conventional notation in the sense that df2o3 6320 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
13-Jul-2022 | enomnilem 7003 | Lemma for enomni 7004. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni Omni | ||
13-Jul-2022 | isomnimap 7002 | The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.) |
Omni | ||
12-Jul-2022 | finexdc 6789 | Decidability of existence, over a finite set and defined by a decidable proposition. (Contributed by Jim Kingdon, 12-Jul-2022.) |
DECID DECID | ||
11-Jul-2022 | dfrex2fin 6790 | Relationship between universal and existential quantifiers over a finite set. Remark in Section 2.2.1 of [Pierik], p. 8. Although Pierik does not mention the decidability condition explicitly, it does say "only finitely many x to check" which means there must be some way of checking each value of x. (Contributed by Jim Kingdon, 11-Jul-2022.) |
DECID | ||
10-Jul-2022 | djuinj 6984 | The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
⊔d | ||
10-Jul-2022 | djudm 6983 | The domain of the "domain-disjoint-union" is the disjoint union of the domains. Remark: its range is the (standard) union of the ranges. (Contributed by BJ, 10-Jul-2022.) |
⊔d ⊔ | ||
10-Jul-2022 | djufun 6982 | The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊔d | ||
10-Jul-2022 | df-djud 6981 |
The "domain-disjoint-union" of two relations: if and
are two binary relations,
then ⊔d is the
binary relation from ⊔
to having the universal
property of disjoint unions (see updjud 6960 in the case of functions).
Remark: the restrictions to (resp. ) are not necessary since extra stuff would be thrown away in the post-composition with (resp. ), as in df-case 6962, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.) |
⊔d inl inr | ||
10-Jul-2022 | casef1 6968 | The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
10-Jul-2022 | caseinj 6967 | The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
case | ||
10-Jul-2022 | casef 6966 | The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
10-Jul-2022 | caserel 6965 | The "case" construction of two relations is a relation, with bounds on its domain and codomain. Typically, the "case" construction is used when both relations have a common codomain. (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
10-Jul-2022 | casedm 6964 | The domain of the "case" construction is the disjoint union of the domains. TODO (although less important): case . (Contributed by BJ, 10-Jul-2022.) |
case ⊔ | ||
10-Jul-2022 | casefun 6963 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
case | ||
10-Jul-2022 | df-case 6962 | The "case" construction: if and are functions, then case ⊔ is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions updjud 6960. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.) |
case inl inr | ||
10-Jul-2022 | cocnvss 5059 | Upper bound for the composed of a relation and an inverse relation. (Contributed by BJ, 10-Jul-2022.) |
10-Jul-2022 | cocnvres 5058 | Restricting a relation and a converse relation when they are composed together (Contributed by BJ, 10-Jul-2022.) |
10-Jul-2022 | cossxp2 5057 | The composition of two relations is a relation, with bounds on its domain and codomain. (Contributed by BJ, 10-Jul-2022.) |
10-Jul-2022 | rnxpss2 4967 | Upper bound for the range of a binary relation. (Contributed by BJ, 10-Jul-2022.) |
10-Jul-2022 | dmxpss2 4966 | Upper bound for the domain of a binary relation. (Contributed by BJ, 10-Jul-2022.) |
10-Jul-2022 | elco 4700 | Elements of a composed relation. (Contributed by BJ, 10-Jul-2022.) |
9-Jul-2022 | geoihalfsum 11284 | Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 11281. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 11283 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by AV, 9-Jul-2022.) |
9-Jul-2022 | exmidfodomrlemrALT 7052 | The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7051. In particular, this proof uses eldju 6946 instead of djur 6947 and avoids djulclb 6933. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
EXMID | ||
9-Jul-2022 | exmidfodomrlemreseldju 7049 | Lemma for exmidfodomrlemrALT 7052. A variant of eldju 6946. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊔ inl inr | ||
8-Jul-2022 | abn0m 3383 | Inhabited class abstraction. (Contributed by Jim Kingdon, 8-Jul-2022.) |
7-Jul-2022 | fvco4 5486 | Value of a composition. (Contributed by BJ, 7-Jul-2022.) |
6-Jul-2022 | toponrestid 12177 | Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.) |
TopOn ↾t | ||
6-Jul-2022 | djuunr 6944 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.) |
inl inr ⊔ | ||
6-Jul-2022 | djurclr 6928 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
inr ⊔ | ||
6-Jul-2022 | djulclr 6927 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
inl ⊔ | ||
6-Jul-2022 | foelrn 5647 | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) (Proof shortened by BJ, 6-Jul-2022.) |
6-Jul-2022 | foima2 5646 | Given an onto function, an element is in its codomain if and only if it is the image of an element of its domain (see foima 5345). (Contributed by BJ, 6-Jul-2022.) |
6-Jul-2022 | f1rn 5324 | The range of a one-to-one mapping. (Contributed by BJ, 6-Jul-2022.) |
5-Jul-2022 | distspace 12493 | A set together with a (distance) function which is a pseudometric is a distance space (according to E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006), i.e. a (base) set equipped with a distance , which is a mapping of two elements of the base set to the (extended) reals and which is nonnegative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021.) (Revised by AV, 5-Jul-2022.) |
PsMet | ||
4-Jul-2022 | djurclALT 12998 | Shortening of djurcl 6930 using djucllem 12996. (Contributed by BJ, 4-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
inr ⊔ | ||
4-Jul-2022 | djulclALT 12997 | Shortening of djulcl 6929 using djucllem 12996. (Contributed by BJ, 4-Jul-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
inl ⊔ | ||
4-Jul-2022 | djucllem 12996 | Lemma for djulcl 6929 and djurcl 6930. (Contributed by BJ, 4-Jul-2022.) |
4-Jul-2022 | inresflem 6938 | Lemma for inlresf1 6939 and inrresf1 6940. (Contributed by BJ, 4-Jul-2022.) |
4-Jul-2022 | djuf1olemr 6932 | Lemma for djulf1or 6934 and djurf1or 6935. For a version of this lemma with defined on and no restriction in the conclusion, see djuf1olem 6931. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
4-Jul-2022 | djuf1olem 6931 | Lemma for djulf1o 6936 and djurf1o 6937. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
4-Jul-2022 | snexxph 6831 | A case where the antecedent of snexg 4103 is not needed. The class is from dcextest 4490. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.) |
4-Jul-2022 | 1oex 6314 | Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.) |
4-Jul-2022 | resflem 5577 | A lemma to bound the range of a restriction. The conclusion would also hold with in place of (provided does not occur in ). If that stronger result is needed, it is however simpler to use the instance of resflem 5577 where is substituted for (in both the conclusion and the third hypothesis). (Contributed by BJ, 4-Jul-2022.) |
4-Jul-2022 | f1ff1 5331 | If a function is one-to-one from A to B and is also a function from A to C, then it is a one-to-one function from A to C. (Contributed by BJ, 4-Jul-2022.) |
3-Jul-2022 | fnmpoovd 6105 | A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019.) (Revised by AV, 3-Jul-2022.) |
3-Jul-2022 | dcextest 4490 | If it is decidable whether is a set, then is decidable (where does not occur in ). From this fact, we can deduce (outside the formal system, since we cannot quantify over classes) that if it is decidable whether any class is a set, then "weak excluded middle" (that is, any negated proposition is decidable) holds. (Contributed by Jim Kingdon, 3-Jul-2022.) |
DECID DECID | ||
3-Jul-2022 | notnotsnex 4106 | A singleton is never a proper class. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jul-2022.) |
2-Jul-2022 | exmidfodomrlemeldju 7048 | Lemma for exmidfodomr 7053. A variant of djur 6947. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊔ inl inr | ||
2-Jul-2022 | djune 6956 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
inl inr | ||
2-Jul-2022 | djulclb 6933 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
inl ⊔ | ||
1-Jul-2022 | exmidfodomr 7053 | Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.) |
EXMID | ||
1-Jul-2022 | exmidfodomrlemr 7051 | The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.) |
EXMID | ||
1-Jul-2022 | exmidfodomrlemim 7050 | Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.) |
EXMID | ||
1-Jul-2022 | dju1p1e2 7046 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊔ | ||
1-Jul-2022 | notm0 3378 | A class is not inhabited if and only if it is empty. (Contributed by Jim Kingdon, 1-Jul-2022.) |
30-Jun-2022 | exmidomni 7007 | Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.) |
EXMID Omni | ||
30-Jun-2022 | exmidpw 6795 | Excluded middle is equivalent to the power set of having two elements. Remark of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 30-Jun-2022.) |
EXMID | ||
29-Jun-2022 | exmidomniim 7006 | Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7007. (Contributed by Jim Kingdon, 29-Jun-2022.) |
EXMID Omni | ||
29-Jun-2022 | dfrex2dc 2426 | Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.) |
DECID | ||
28-Jun-2022 | finomni 7005 | A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
28-Jun-2022 | isomni 7001 | The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
28-Jun-2022 | df-omni 6999 |
An omniscient set is one where we can decide whether a predicate (here
represented by a function ) holds (is equal to ) for all
elements or fails to hold (is equal to ) for some element.
Definition 3.1 of [Pierik], p. 14.
In particular, Omni is known as the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.) |
Omni | ||
28-Jun-2022 | updjud 6960 | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
⊔ inl inr | ||
28-Jun-2022 | inrresf1 6940 | The right injection restricted to the right class of a disjoint union is an injective function from the right class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
inr ⊔ | ||
28-Jun-2022 | inlresf1 6939 | The left injection restricted to the left class of a disjoint union is an injective function from the left class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
inl ⊔ | ||
28-Jun-2022 | djuex 6921 | The disjoint union of sets is a set. See also the more precise djuss 6948. (Contributed by AV, 28-Jun-2022.) |
⊔ | ||
28-Jun-2022 | f1resf1 5333 | The restriction of an injective function is injective. (Contributed by AV, 28-Jun-2022.) |
27-Jun-2022 | updjudhcoinrg 6959 | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.) |
⊔ inr | ||
27-Jun-2022 | updjudhcoinlf 6958 | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.) |
⊔ inl | ||
27-Jun-2022 | 2ndinr 6955 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
inr | ||
27-Jun-2022 | 1stinr 6954 | The first component of the value of a right injection is . (Contributed by AV, 27-Jun-2022.) |
inr | ||
27-Jun-2022 | 2ndinl 6953 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
inl | ||
27-Jun-2022 | 1stinl 6952 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
inl | ||
26-Jun-2022 | updjudhf 6957 | The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.) |
⊔ ⊔ | ||
26-Jun-2022 | eldju2ndr 6951 | The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.) |
⊔ | ||
26-Jun-2022 | eldju2ndl 6950 | The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.) |
⊔ | ||
26-Jun-2022 | eldju1st 6949 | The first component of an element of a disjoint union is either or . (Contributed by AV, 26-Jun-2022.) |
⊔ | ||
25-Jun-2022 | djuss 6948 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊔ | ||
23-Jun-2022 | eldju 6946 | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊔ inl inr | ||
23-Jun-2022 | nfdju 6920 | Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ | ||
23-Jun-2022 | djueq2 6919 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ ⊔ | ||
23-Jun-2022 | djueq1 6918 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ ⊔ | ||
23-Jun-2022 | djueq12 6917 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊔ ⊔ | ||
22-Jun-2022 | djurf1o 6937 | The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
inr | ||
22-Jun-2022 | djulf1o 6936 | The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
inl | ||
22-Jun-2022 | djurf1or 6935 | The right injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.) |
inr | ||
22-Jun-2022 | djulf1or 6934 | The left injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.) |
inl | ||
21-Jun-2022 | djuinr 6941 | The ranges of any left and right injections are disjoint. Remark: the extra generality offered by the two restrictions makes the theorem more readily usable (e.g., by djudom 6971 and djufun 6982) while the simpler statement inl inr is easily recovered from it by substituting for both and as done in casefun 6963). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
inl inr | ||
21-Jun-2022 | djurcl 6930 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inr ⊔ | ||
21-Jun-2022 | djulcl 6929 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
inl ⊔ | ||
21-Jun-2022 | df-inr 6926 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
inr | ||
21-Jun-2022 | df-inl 6925 | Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
inl | ||
20-Jun-2022 | df-dju 6916 | Disjoint union of two classes. This is a way of creating a class which contains elements corresponding to each element of or , tagging each one with whether it came from or . (Contributed by Jim Kingdon, 20-Jun-2022.) |
⊔ | ||
18-Jun-2022 | exmidundif 4124 | Excluded middle is equivalent to every subset having a complement. That is, the union of a subset and its relative complement being the whole set. Although special cases such as undifss 3438 and undifdcss 6804 are provable, the full statement is equivalent to excluded middle as shown here. (Contributed by Jim Kingdon, 18-Jun-2022.) |
EXMID | ||
18-Jun-2022 | exmidel 4123 | Excluded middle is equivalent to decidability of membership for two arbitrary sets. (Contributed by Jim Kingdon, 18-Jun-2022.) |
EXMID DECID | ||
18-Jun-2022 | exmid0el 4122 | Excluded middle is equivalent to decidability of being an element of an arbitrary set. (Contributed by Jim Kingdon, 18-Jun-2022.) |
EXMID DECID | ||
18-Jun-2022 | exmid01 4116 | Excluded middle is equivalent to saying any subset of is either or . (Contributed by BJ and Jim Kingdon, 18-Jun-2022.) |
EXMID | ||
18-Jun-2022 | exmidexmid 4115 |
EXMID implies that an arbitrary proposition is decidable. That is,
EXMID captures the usual meaning of excluded middle when stated in terms
of propositions.
To get other propositional statements which are equivalent to excluded middle, combine this with notnotrdc 828, peircedc 899, or condc 838. (Contributed by Jim Kingdon, 18-Jun-2022.) |
EXMID DECID | ||
18-Jun-2022 | df-exmid 4114 |
The expression EXMID will be used as a readable shorthand for
any
form of the law of the excluded middle; this is a useful shorthand
largely because it hides statements of the form "for any
proposition" in
a system which can only quantify over sets, not propositions.
To see how this compares with other ways of expressing excluded middle, compare undifexmid 4112 with exmidundif 4124. The former may be more recognizable as excluded middle because it is in terms of propositions, and the proof may be easier to follow for much the same reason (it just has to show and in the the relevant parts of the proof). The latter, however, has the key advantage of being able to prove both directions of the biconditional. To state that excluded middle implies a proposition is hard to do gracefully without EXMID, because there is no way to write a hypothesis for an arbitrary proposition; instead the hypothesis would need to be the particular instance of excluded middle which that proof needs. Or to say it another way, EXMID implies DECID by exmidexmid 4115 but there is no good way to express the converse. This definition and how we use it is easiest to understand (and most appropriate to assign the name "excluded middle" to) if we assume ax-sep 4041, in which case EXMID means that all propositions are decidable (see exmidexmid 4115 and notice that it relies on ax-sep 4041). If we instead work with ax-bdsep 13071, EXMID as defined here means that all bounded propositions are decidable. (Contributed by Mario Carneiro and Jim Kingdon, 18-Jun-2022.) |
EXMID DECID | ||
17-Jun-2022 | undifdc 6805 | Union of complementary parts into whole. This is a case where we can strengthen undifss 3438 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
17-Jun-2022 | undifdcss 6804 | Union of complementary parts into whole and decidability. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
17-Jun-2022 | dcdifsnid 6393 | If we remove a single element from a set with decidable equality then put it back in, we end up with the original set. This strengthens difsnss 3661 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 17-Jun-2022.) |
DECID | ||
16-Jun-2022 | undifexmid 4112 | Union of complementary parts producing the whole and excluded middle. Although special cases such as undifss 3438 and undifdcss 6804 are provable, the full statement implies excluded middle as shown here. (Contributed by Jim Kingdon, 16-Jun-2022.) |
16-Jun-2022 | dfdif3 3181 | Alternate definition of class difference. Definition of relative set complement in Section 2.3 of [Pierik], p. 10. (Contributed by BJ and Jim Kingdon, 16-Jun-2022.) |
15-Jun-2022 | inffiexmid 6793 | If any given set is either finite or infinite, excluded middle follows. (Contributed by Jim Kingdon, 15-Jun-2022.) |
15-Jun-2022 | isinfinf 6784 | An infinite set contains subsets of arbitrarily large finite cardinality. (Contributed by Jim Kingdon, 15-Jun-2022.) |
5-Jun-2022 | dif1enen 6767 | Subtracting one element from each of two equinumerous finite sets. (Contributed by Jim Kingdon, 5-Jun-2022.) |
3-Jun-2022 | ifbothdadc 3498 | A formula containing a decidable conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 3-Jun-2022.) |
DECID | ||
31-May-2022 | fihashssdif 10557 | The size of the difference of a finite set and a finite subset is the set's size minus the subset's. (Contributed by Jim Kingdon, 31-May-2022.) |
♯ ♯ ♯ | ||
31-May-2022 | prfidisj 6808 | A pair is finite if it consists of two unequal sets. For the case where , see snfig 6701. For the cases where one or both is a proper class, see prprc1 3626, prprc2 3627, or prprc 3628. (Contributed by Jim Kingdon, 31-May-2022.) |
31-May-2022 | ssdifsn 3646 | Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.) |
28-May-2022 | phivalfi 11877 | Finiteness of an expression used to define the Euler function. (Contributed by Jim Kingon, 28-May-2022.) |
27-May-2022 | ssfidc 6816 | A subset of a finite set is finite if membership in the subset is decidable. (Contributed by Jim Kingdon, 27-May-2022.) |
DECID | ||
27-May-2022 | ssfirab 6815 | A subset of a finite set is finite if it is defined by a decidable property. (Contributed by Jim Kingdon, 27-May-2022.) |
DECID | ||
24-May-2022 | nn0sqrtelqelz 11873 | If a nonnegative integer has a rational square root, that root must be an integer. (Contributed by Jim Kingdon, 24-May-2022.) |
15-May-2022 | oawordriexmid 6359 | A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6358. (Contributed by Jim Kingdon, 15-May-2022.) |
13-May-2022 | unennn 11899 | The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.) |
12-May-2022 | evenennn 11895 | There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.) |
11-May-2022 | oddennn 11894 | There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.) |
11-May-2022 | flapcl 10041 | The floor (greatest integer) function yields an integer when applied to a real number apart from any integer. For example, an irrational number (see for example sqrt2irrap 11847) would satisfy this condition. (Contributed by Jim Kingdon, 11-May-2022.) |
# | ||
11-May-2022 | apbtwnz 10040 | There is a unique greatest integer less than or equal to a real number which is apart from all integers. (Contributed by Jim Kingdon, 11-May-2022.) |
# | ||
10-May-2022 | exbtwnz 10021 | If a real number is between an integer and its successor, there is a unique greatest integer less than or equal to the real number. (Contributed by Jim Kingdon, 10-May-2022.) |
10-May-2022 | exbtwnzlemshrink 10019 | Lemma for exbtwnzlemex 10020. Shrinking the range around . (Contributed by Jim Kingdon, 10-May-2022.) |
10-May-2022 | exbtwnzlemstep 10018 | Lemma for exbtwnzlemex 10020. Induction step. (Contributed by Jim Kingdon, 10-May-2022.) |
30-Apr-2022 | seq3p1 10228 | Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 30-Apr-2022.) |
29-Apr-2022 | frecuzrdgsuct 10190 | Successor value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 29-Apr-2022.) |
frec | ||
29-Apr-2022 | frecuzrdgsuctlem 10189 | Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 10165 for the description of as the mapping from to . (Contributed by Jim Kingdon, 29-Apr-2022.) |
frec frec | ||
28-Apr-2022 | iseqvalcbv 10223 | Changing the bound variables in an expression which appears in some related proofs. (Contributed by Jim Kingdon, 28-Apr-2022.) |
frec frec | ||
28-Apr-2022 | frecuzrdg0t 10188 | Initial value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 28-Apr-2022.) |
frec | ||
24-Apr-2022 | frecuzrdgfun 10186 | The recursive definition generator on upper integers produces a a function. (Contributed by Jim Kingdon, 24-Apr-2022.) |
frec | ||
24-Apr-2022 | frecuzrdgfunlem 10185 | The recursive definition generator on upper integers produces a a function. (Contributed by Jim Kingdon, 24-Apr-2022.) |
frec frec | ||
24-Apr-2022 | frecuzrdgdom 10184 | The domain of the result of the recursive definition generator on upper integers. (Contributed by Jim Kingdon, 24-Apr-2022.) |
frec | ||
24-Apr-2022 | frecuzrdgdomlem 10183 | The domain of the result of the recursive definition generator on upper integers. (Contributed by Jim Kingdon, 24-Apr-2022.) |
frec frec | ||
23-Apr-2022 | frecuzrdgg 10182 | Lemma for other theorems involving the the recursive definition generator on upper integers. Evaluating at a natural number gives an ordered pair whose first element is the mapping of that natural number via . (Contributed by Jim Kingdon, 23-Apr-2022.) |
frec frec | ||
22-Apr-2022 | frecuzrdgtclt 10187 | The recursive definition generator on upper integers is a function. (Contributed by Jim Kingdon, 22-Apr-2022.) |
frec | ||
22-Apr-2022 | frecuzrdgrclt 10181 | The function (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of . Similar to frecuzrdgrcl 10176 except that and need not be the same. (Contributed by Jim Kingdon, 22-Apr-2022.) |
frec | ||
17-Apr-2022 | funinsn 5167 | A function based on the singleton of an ordered pair. Unlike funsng 5164, this holds even if or is a proper class. (Contributed by Jim Kingdon, 17-Apr-2022.) |
14-Apr-2022 | ad4ant234 1196 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad4ant134 1195 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad4ant124 1194 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad4ant123 1193 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad5ant25 515 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad5ant24 514 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad5ant23 513 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad5ant15 512 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad5ant14 511 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad5ant13 510 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad4ant24 507 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad4ant23 506 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad4ant14 505 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
14-Apr-2022 | ad4ant13 504 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
13-Apr-2022 | rdgon 6276 | Evaluating the recursive definition generator produces an ordinal. There is a hypothesis that the characteristic function produces ordinals on ordinal arguments. (Contributed by Jim Kingdon, 26-Jul-2019.) (Revised by Jim Kingdon, 13-Apr-2022.) |
1-Apr-2022 | frecuzrdgrcl 10176 | The function (used in the definition of the recursive definition generator on upper integers) is a function defined for all natural numbers. (Contributed by Jim Kingdon, 1-Apr-2022.) |
frec frec | ||
31-Mar-2022 | frecsuc 6297 | The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 31-Mar-2022.) |
frec frec | ||
30-Mar-2022 | frecfcl 6295 | Finite recursion yields a function on the natural numbers. (Contributed by Jim Kingdon, 30-Mar-2022.) |
frec | ||
30-Mar-2022 | frecfcllem 6294 | Lemma for frecfcl 6295. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 30-Mar-2022.) |
recs frec | ||
29-Mar-2022 | frecsuclem 6296 | Lemma for frecsuc 6297. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 29-Mar-2022.) |
frec frec | ||
28-Mar-2022 | frecuzrdgrrn 10174 | The function (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of . (Contributed by Jim Kingdon, 28-Mar-2022.) |
frec frec | ||
27-Mar-2022 | freccl 6293 | Closure for finite recursion. (Contributed by Jim Kingdon, 27-Mar-2022.) |
frec | ||
27-Mar-2022 | freccllem 6292 | Lemma for freccl 6293. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 27-Mar-2022.) |
recs frec | ||
26-Mar-2022 | tfrcldm 6253 | Recursion is defined on an ordinal if the characteristic function satisfies a closure hypothesis up to a suitable point. (Contributed by Jim Kingdon, 26-Mar-2022.) |
recs | ||
26-Mar-2022 | tfrcllemaccex 6251 |
We can define an acceptable function on any element of .
As with many of the transfinite recursion theorems, we have hypotheses that state that is a function and that it is defined up to . (Contributed by Jim Kingdon, 26-Mar-2022.) |
recs | ||
26-Mar-2022 | tfrcllemex 6250 | Lemma for tfrcl 6254. (Contributed by Jim Kingdon, 26-Mar-2022.) |
recs | ||
25-Mar-2022 | tfrcl 6254 | Closure for transfinite recursion. As with tfr1on 6240, the characteristic function must be defined up to a suitable point, not necessarily on all ordinals. (Contributed by Jim Kingdon, 25-Mar-2022.) |
recs | ||
25-Mar-2022 | tfrcllemubacc 6249 | Lemma for tfrcl 6254. The union of satisfies the recursion rule. (Contributed by Jim Kingdon, 25-Mar-2022.) |
recs | ||
25-Mar-2022 | tfrcllembex 6248 | Lemma for tfrcl 6254. The set exists. (Contributed by Jim Kingdon, 25-Mar-2022.) |
recs | ||
25-Mar-2022 | tfrcllembfn 6247 | Lemma for tfrcl 6254. The union of is a function defined on . (Contributed by Jim Kingdon, 25-Mar-2022.) |
recs | ||
25-Mar-2022 | tfrcllembxssdm 6246 | Lemma for tfrcl 6254. The union of is defined on all elements of . (Contributed by Jim Kingdon, 25-Mar-2022.) |
recs | ||
25-Mar-2022 | tfrcllembacc 6245 | Lemma for tfrcl 6254. Each element of is an acceptable function. (Contributed by Jim Kingdon, 25-Mar-2022.) |
recs | ||
25-Mar-2022 | tfrcllemssrecs 6242 | Lemma for tfrcl 6254. The union of functions acceptable for tfrcl 6254 is a subset of recs. (Contributed by Jim Kingdon, 25-Mar-2022.) |
recs | ||
24-Mar-2022 | tfrcllemsucaccv 6244 | Lemma for tfrcl 6254. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 24-Mar-2022.) |
recs | ||
24-Mar-2022 | tfrcllemsucfn 6243 | We can extend an acceptable function by one element to produce a function. Lemma for tfrcl 6254. (Contributed by Jim Kingdon, 24-Mar-2022.) |
recs | ||
21-Mar-2022 | frecabcl 6289 | The class abstraction from df-frec 6281 exists. Unlike frecabex 6288 the function only needs to be defined on , not all sets. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 21-Mar-2022.) |
20-Mar-2022 | tfri1dALT 6241 |
Alternate proof of tfri1d 6225 in terms of tfr1on 6240.
Although this does show that the tfr1on 6240 proof is general enough to also prove tfri1d 6225, the tfri1d 6225 proof is simpler in places because it does not need to deal with being any ordinal. For that reason, we have both proofs. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by Jim Kingdon, 20-Mar-2022.) |
recs | ||
18-Mar-2022 | tfrcllemres 6252 | Lemma for tfr1on 6240. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.) |
recs | ||
18-Mar-2022 | tfr1onlemres 6239 | Lemma for tfr1on 6240. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.) |
recs | ||
16-Mar-2022 | tfr1onlemaccex 6238 |
We can define an acceptable function on any element of .
As with many of the transfinite recursion theorems, we have hypotheses that state that is a function and that it is defined up to . (Contributed by Jim Kingdon, 16-Mar-2022.) |
recs | ||
16-Mar-2022 | tfr1onlemex 6237 | Lemma for tfr1on 6240. (Contributed by Jim Kingdon, 16-Mar-2022.) |
recs | ||
15-Mar-2022 | tfr1onlemubacc 6236 | Lemma for tfr1on 6240. The union of satisfies the recursion rule. (Contributed by Jim Kingdon, 15-Mar-2022.) |
recs | ||
15-Mar-2022 | tfr1onlembfn 6234 | Lemma for tfr1on 6240. The union of is a function defined on . (Contributed by Jim Kingdon, 15-Mar-2022.) |
recs | ||
15-Mar-2022 | tfr1onlemssrecs 6229 | Lemma for tfr1on 6240. The union of functions acceptable for tfr1on 6240 is a subset of recs. (Contributed by Jim Kingdon, 15-Mar-2022.) |
recs | ||
14-Mar-2022 | tfr1onlembex 6235 | Lemma for tfr1on 6240. The set exists. (Contributed by Jim Kingdon, 14-Mar-2022.) |
recs | ||
14-Mar-2022 | tfr1onlembxssdm 6233 | Lemma for tfr1on 6240. The union of is defined on all elements of . (Contributed by Jim Kingdon, 14-Mar-2022.) |
recs | ||
14-Mar-2022 | tfr1onlembacc 6232 | Lemma for tfr1on 6240. Each element of is an acceptable function. (Contributed by Jim Kingdon, 14-Mar-2022.) |
recs | ||
14-Mar-2022 | tfr1onlem3 6228 | Lemma for transfinite recursion. This lemma changes some bound variables in (version of tfrlem3 6201 but for tfr1on 6240 related lemmas). (Contributed by Jim Kingdon, 14-Mar-2022.) |
13-Mar-2022 | nnsucuniel 6384 | Given an element of the union of a natural number , is an element of itself. The reverse direction holds for all ordinals (sucunielr 4421). The forward direction for all ordinals implies excluded middle (ordsucunielexmid 4441). (Contributed by Jim Kingdon, 13-Mar-2022.) |
13-Mar-2022 | tfr1onlem3ag 6227 | Lemma for transfinite recursion. This lemma changes some bound variables in (version of tfrlem3ag 6199 but for tfr1on 6240 related lemmas). (Contributed by Jim Kingdon, 13-Mar-2022.) |
12-Mar-2022 | tfr1on 6240 | Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 12-Mar-2022.) |
recs | ||
12-Mar-2022 | tfr1onlemsucaccv 6231 | Lemma for tfr1on 6240. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 12-Mar-2022.) |
recs | ||
12-Mar-2022 | tfr1onlemsucfn 6230 | We can extend an acceptable function by one element to produce a function. Lemma for tfr1on 6240. (Contributed by Jim Kingdon, 12-Mar-2022.) |
recs | ||
8-Mar-2022 | tfr0dm 6212 | Transfinite recursion is defined at the empty set. (Contributed by Jim Kingdon, 8-Mar-2022.) |
recs | ||
5-Mar-2022 | unfiexmid 6799 | If the union of any two finite sets is finite, excluded middle follows. Remark 8.1.17 of [AczelRathjen], p. 74. (Contributed by Mario Carneiro and Jim Kingdon, 5-Mar-2022.) |
2-Mar-2022 | unfiin 6807 | The union of two finite sets is finite if their intersection is. (Contributed by Jim Kingdon, 2-Mar-2022.) |
2-Mar-2022 | undiffi 6806 | Union of complementary parts into whole. This is a case where we can strengthen undifss 3438 from subset to equality. (Contributed by Jim Kingdon, 2-Mar-2022.) |
1-Mar-2022 | 1domsn 6706 | A singleton (whether of a set or a proper class) is dominated by one. (Contributed by Jim Kingdon, 1-Mar-2022.) |
25-Feb-2022 | hashunlem 10543 | Lemma for hashun 10544. Ordinal size of the union. (Contributed by Jim Kingdon, 25-Feb-2022.) |
25-Feb-2022 | unfidisj 6803 | The union of two disjoint finite sets is finite. (Contributed by Jim Kingdon, 25-Feb-2022.) |
24-Feb-2022 | fihashdom 10542 | Dominance relation for the size function. (Contributed by Jim Kingdon, 24-Feb-2022.) |
♯ ♯ | ||
24-Feb-2022 | omgadd 10541 | Mapping ordinal addition to integer addition. (Contributed by Jim Kingdon, 24-Feb-2022.) |
frec | ||
24-Feb-2022 | frec2uzled 10195 | The mapping (see frec2uz0d 10165) preserves order. (Contributed by Jim Kingdon, 24-Feb-2022.) |
frec | ||
22-Feb-2022 | isfinite4im 10532 | A finite set is equinumerous to the range of integers from one up to the hash value of the set. (Contributed by Jim Kingdon, 22-Feb-2022.) |
♯ | ||
21-Feb-2022 | filtinf 10531 | The size of an infinite set is greater than the size of a finite set. (Contributed by Jim Kingdon, 21-Feb-2022.) |
♯ ♯ | ||
21-Feb-2022 | fihasheqf1od 10529 | The size of two finite sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Jim Kingdon, 21-Feb-2022.) |
♯ ♯ | ||
21-Feb-2022 | fihashf1rn 10528 | The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Jim Kingdon, 21-Feb-2022.) |
♯ ♯ | ||
21-Feb-2022 | fihasheqf1oi 10527 | The size of two finite sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Jim Kingdon, 21-Feb-2022.) |
♯ ♯ | ||
21-Feb-2022 | hashfiv01gt1 10521 | The size of a finite set is either 0 or 1 or greater than 1. (Contributed by Jim Kingdon, 21-Feb-2022.) |
♯ ♯ ♯ | ||
21-Feb-2022 | hashennn 10519 | The size of a set equinumerous to an element of . (Contributed by Jim Kingdon, 21-Feb-2022.) |
♯ frec | ||
21-Feb-2022 | f1ofi 6824 | If a 1-1 and onto function has a finite domain, its range is finite. (Contributed by Jim Kingdon, 21-Feb-2022.) |
20-Feb-2022 | hashennnuni 10518 | The ordinal size of a set equinumerous to an element of is that element of . (Contributed by Jim Kingdon, 20-Feb-2022.) |
20-Feb-2022 | hashinfom 10517 | The value of the ♯ function on an infinite set. (Contributed by Jim Kingdon, 20-Feb-2022.) |
♯ | ||
20-Feb-2022 | hashinfuni 10516 | The ordinal size of an infinite set is . (Contributed by Jim Kingdon, 20-Feb-2022.) |
20-Feb-2022 | infnfi 6782 | An infinite set is not finite. (Contributed by Jim Kingdon, 20-Feb-2022.) |
19-Feb-2022 | sumdc2 12995 | Alternate proof of sumdc 11120, without disjoint variable condition on (longer because the statement is taylored to the proof sumdc 11120). (Contributed by BJ, 19-Feb-2022.) |
DECID DECID | ||
19-Feb-2022 | uzdcinzz 12994 | An upperset of integers is decidable in the integers. Reformulation of eluzdc 9397. (Contributed by Jim Kingdon, 18-Apr-2020.) (Revised by BJ, 19-Feb-2022.) |
DECIDin | ||
19-Feb-2022 | decidin 12993 | If A is a decidable subclass of B (meaning: it is a subclass of B and it is decidable in B), and B is decidable in C, then A is decidable in C. (Contributed by BJ, 19-Feb-2022.) |
DECIDin DECIDin DECIDin | ||
19-Feb-2022 | decidr 12992 | Sufficient condition for being decidable in another class. (Contributed by BJ, 19-Feb-2022.) |
DECIDin | ||
19-Feb-2022 | decidi 12991 | Property of being decidable in another class. (Contributed by BJ, 19-Feb-2022.) |
DECIDin | ||
19-Feb-2022 | df-dcin 12990 | Define decidability of a class in another. (Contributed by BJ, 19-Feb-2022.) |
DECIDin DECID | ||
19-Feb-2022 | df-ihash 10515 |
Define the set size function ♯, which gives the cardinality of a
finite set as a member of , and assigns all infinite sets the
value .
For example, ♯ .
Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8337). We adopt the former notation from Corollary 8.2.4 of [AczelRathjen], p. 80 (although that work only defines it for finite sets). This definition (in terms of and ) is not taken directly from the literature, but for finite sets should be equivalent to the conventional definition that the size of a finite set is the unique natural number which is equinumerous to the given set. (Contributed by Jim Kingdon, 19-Feb-2022.) |
♯ frec | ||
18-Feb-2022 | infm 6791 | An infinite set is inhabited. (Contributed by Jim Kingdon, 18-Feb-2022.) |
13-Feb-2022 | frecfun 6285 | Finite recursion produces a function. See also frecfnom 6291 which also states that the domain of that function is but which puts conditions on and . (Contributed by Jim Kingdon, 13-Feb-2022.) |
frec | ||
12-Feb-2022 | relsnopg 4638 | A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by BJ, 12-Feb-2022.) |
12-Feb-2022 | relsng 4637 | A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.) (Revised by BJ, 12-Feb-2022.) |
10-Feb-2022 | ltmininf 10999 | Two ways of saying a number is less than the minimum of two others. (Contributed by Jim Kingdon, 10-Feb-2022.) |
inf | ||
10-Feb-2022 | maxltsup 10983 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 10-Feb-2022.) |
9-Feb-2022 | xrmaxleastlt 11018 | The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.) |
9-Feb-2022 | maxleastlt 10980 | The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.) |
6-Feb-2022 | unsnfidcel 6802 | The condition in unsnfi 6800. This is intended to show that unsnfi 6800 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.) |
DECID | ||
6-Feb-2022 | unsnfidcex 6801 | The condition in unsnfi 6800. This is intended to show that unsnfi 6800 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.) |
DECID | ||
5-Feb-2022 | funrnfi 6823 | The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.) |
5-Feb-2022 | relcnvfi 6822 | If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.) |
5-Feb-2022 | fundmfi 6819 | The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.) |
5-Feb-2022 | infiexmid 6764 | If the intersection of any finite set and any other set is finite, excluded middle follows. (Contributed by Jim Kingdon, 5-Feb-2022.) |
3-Feb-2022 | unsnfi 6800 | Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.) |
3-Feb-2022 | domfiexmid 6765 | If any set dominated by a finite set is finite, excluded middle follows. (Contributed by Jim Kingdon, 3-Feb-2022.) |
3-Feb-2022 | ssfilem 6762 | Lemma for ssfiexmid 6763. (Contributed by Jim Kingdon, 3-Feb-2022.) |
1-Feb-2022 | maxclpr 10987 | The maximum of two real numbers is one of those numbers if and only if dichotomy ( ) holds. For example, this can be combined with zletric 9091 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 1-Feb-2022.) |
31-Jan-2022 | znege1 11845 | The absolute value of the difference between two unequal integers is at least one. (Contributed by Jim Kingdon, 31-Jan-2022.) |
31-Jan-2022 | maxleastb 10979 | Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Jim Kingdon, 31-Jan-2022.) |
30-Jan-2022 | max0addsup 10984 | The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.) |
29-Jan-2022 | expcanlem 10455 | Lemma for expcan 10456. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.) |
28-Jan-2022 | exfzdc 10010 | Decidability of the existence of an integer defined by a decidable proposition. (Contributed by Jim Kingdon, 28-Jan-2022.) |
DECID DECID | ||
25-Jan-2022 | 1nen2 6748 | One and two are not equinumerous. (Contributed by Jim Kingdon, 25-Jan-2022.) |
24-Jan-2022 | divmulasscomap 8449 | An associative/commutative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.) |
# | ||
24-Jan-2022 | divmulassap 8448 | An associative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.) |
# | ||
21-Jan-2022 | lcmmndc 11732 | Decidablity lemma used in various proofs related to lcm. (Contributed by Jim Kingdon, 21-Jan-2022.) |
DECID | ||
20-Jan-2022 | infssuzcldc 11633 | The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.) |
DECID inf | ||
19-Jan-2022 | suprnubex 8704 | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by Jim Kingdon, 19-Jan-2022.) |
19-Jan-2022 | suprlubex 8703 | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by Jim Kingdon, 19-Jan-2022.) |
18-Jan-2022 | suprubex 8702 | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by Jim Kingdon, 18-Jan-2022.) |
17-Jan-2022 | zdvdsdc 11503 | Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.) |
DECID | ||
17-Jan-2022 | suplub2ti 6881 | Bidirectional form of suplubti 6880. (Contributed by Jim Kingdon, 17-Jan-2022.) |
16-Jan-2022 | zssinfcl 11630 | The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
inf inf | ||
16-Jan-2022 | supelti 6882 | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
15-Jan-2022 | infsupneg 9384 | If a set of real numbers has a greatest lower bound, the set of the negation of those numbers has a least upper bound. To go in the other direction see supinfneg 9383. (Contributed by Jim Kingdon, 15-Jan-2022.) |
15-Jan-2022 | supinfneg 9383 | If a set of real numbers has a least upper bound, the set of the negation of those numbers has a greatest lower bound. For a theorem which is similar but only for the boundedness part, see ublbneg 9398. (Contributed by Jim Kingdon, 15-Jan-2022.) |
14-Jan-2022 | supminfex 9385 | A supremum is the negation of the infimum of that set's image under negation. (Contributed by Jim Kingdon, 14-Jan-2022.) |
inf | ||
14-Jan-2022 | infrenegsupex 9382 | The infimum of a set of reals is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 14-Jan-2022.) |
inf | ||
13-Jan-2022 | infssuzledc 11632 | The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by Jim Kingdon, 13-Jan-2022.) |
DECID inf | ||
13-Jan-2022 | infssuzex 11631 | Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.) |
DECID | ||
11-Jan-2022 | ifcldadc 3496 | Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.) |
DECID | ||
9-Jan-2022 | bezoutlemsup 11686 | Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the supremum of divisors of both and . (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
9-Jan-2022 | bezoutlemle 11685 | Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the largest number which divides both and . (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
9-Jan-2022 | bezoutlemeu 11684 | Lemma for Bézout's identity. There is exactly one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
9-Jan-2022 | bezoutlemmo 11683 | Lemma for Bézout's identity. There is at most one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
9-Jan-2022 | hash2iun1dif1 11242 | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
Disj Disj ♯ ♯ ♯ ♯ | ||
9-Jan-2022 | hash2iun 11241 | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
Disj Disj ♯ ♯ | ||
8-Jan-2022 | bezoutlembi 11682 | Lemma for Bézout's identity. Like bezoutlembz 11681 but the greatest common divisor condition is a biconditional, not just an implication. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
8-Jan-2022 | bezoutlembz 11681 | Lemma for Bézout's identity. Like bezoutlemaz 11680 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
8-Jan-2022 | bezoutlemaz 11680 | Lemma for Bézout's identity. Like bezoutlemzz 11679 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
8-Jan-2022 | bezoutlemzz 11679 | Lemma for Bézout's identity. Like bezoutlemex 11678 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
7-Jan-2022 | fsumdifsnconst 11217 | The sum of constant terms ( is not free in ) over an index set excluding a singleton. (Contributed by AV, 7-Jan-2022.) |
♯ | ||
6-Jan-2022 | bezoutlemnewy 11673 | Lemma for Bézout's identity. The is-bezout predicate holds for . (Contributed by Jim Kingdon, 6-Jan-2022.) |
6-Jan-2022 | apsub1 8397 | Subtraction respects apartness. Analogue of subcan2 7980 for apartness. (Contributed by Jim Kingdon, 6-Jan-2022.) |
# # | ||
5-Jan-2022 | eirraplem 11472 | Lemma for eirrap 11473. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.) |
# | ||
3-Jan-2022 | bezoutlemex 11678 | Lemma for Bézout's identity. Existence of a number which we will later show to be the greater common divisor and its decomposition into cofactors. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jan-2022.) |
3-Jan-2022 | bezoutlemstep 11674 | Lemma for Bézout's identity. This is the induction step for the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.) |
2-Jan-2022 | ssrind 3298 | Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
2-Jan-2022 | rexlimdva2 2550 | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
Copyright terms: Public domain | W3C HTML validation [external] |