Home | Intuitionistic Logic Explorer Theorem List (p. 75 of 132) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | recexprlemopl 7401* | The lower cut of is open. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemlol 7402* | The lower cut of is lower. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemopu 7403* | The upper cut of is open. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemupu 7404* | The upper cut of is upper. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 28-Dec-2019.) |
Theorem | recexprlemrnd 7405* | is rounded. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemdisj 7406* | is disjoint. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemloc 7407* | is located. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlempr 7408* | is a positive real. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlem1ssl 7409* | The lower cut of one is a subset of the lower cut of . Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlem1ssu 7410* | The upper cut of one is a subset of the upper cut of . Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemss1l 7411* | The lower cut of is a subset of the lower cut of one. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemss1u 7412* | The upper cut of is a subset of the upper cut of one. Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexprlemex 7413* | is the reciprocal of . Lemma for recexpr 7414. (Contributed by Jim Kingdon, 27-Dec-2019.) |
Theorem | recexpr 7414* | The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
Theorem | aptiprleml 7415 | Lemma for aptipr 7417. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | aptiprlemu 7416 | Lemma for aptipr 7417. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | aptipr 7417 | Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.) |
Theorem | ltmprr 7418 | Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.) |
Theorem | archpr 7419* | For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer is embedded into the reals as described at nnprlu 7329. (Contributed by Jim Kingdon, 22-Apr-2020.) |
Theorem | caucvgprlemcanl 7420* | Lemma for cauappcvgprlemladdrl 7433. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
Theorem | cauappcvgprlemm 7421* | Lemma for cauappcvgpr 7438. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemopl 7422* | Lemma for cauappcvgpr 7438. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemlol 7423* | Lemma for cauappcvgpr 7438. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemopu 7424* | Lemma for cauappcvgpr 7438. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemupu 7425* | Lemma for cauappcvgpr 7438. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemrnd 7426* | Lemma for cauappcvgpr 7438. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemdisj 7427* | Lemma for cauappcvgpr 7438. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemloc 7428* | Lemma for cauappcvgpr 7438. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemcl 7429* | Lemma for cauappcvgpr 7438. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgprlemladdfu 7430* | Lemma for cauappcvgprlemladd 7434. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdfl 7431* | Lemma for cauappcvgprlemladd 7434. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdru 7432* | Lemma for cauappcvgprlemladd 7434. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdrl 7433* | Lemma for cauappcvgprlemladd 7434. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladd 7434* | Lemma for cauappcvgpr 7438. This takes and offsets it by the positive fraction . (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem1 7435* | Lemma for cauappcvgpr 7438. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem2 7436* | Lemma for cauappcvgpr 7438. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlemlim 7437* | Lemma for cauappcvgpr 7438. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgpr 7438* |
A Cauchy approximation has a limit. A Cauchy approximation, here
, is similar
to a Cauchy sequence but is indexed by the desired
tolerance (that is, how close together terms needs to be) rather than
by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p.
(varies) with a few differences such as that we are proving the
existence of a limit without anything about how fast it converges
(that is, mere existence instead of existence, in HoTT terms), and
that the codomain of is
rather than . We
also
specify that every term needs to be larger than a fraction , to
avoid the case where we have positive terms which "converge"
to zero
(which is not a positive real).
This proof (including its lemmas) is similar to the proofs of caucvgpr 7458 and caucvgprpr 7488 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) |
Theorem | archrecnq 7439* | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | archrecpr 7440* | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprlemk 7441 | Lemma for caucvgpr 7458. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemnkj 7442* | Lemma for caucvgpr 7458. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
Theorem | caucvgprlemnbj 7443* | Lemma for caucvgpr 7458. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
Theorem | caucvgprlemm 7444* | Lemma for caucvgpr 7458. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemopl 7445* | Lemma for caucvgpr 7458. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemlol 7446* | Lemma for caucvgpr 7458. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemopu 7447* | Lemma for caucvgpr 7458. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemupu 7448* | Lemma for caucvgpr 7458. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemrnd 7449* | Lemma for caucvgpr 7458. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemdisj 7450* | Lemma for caucvgpr 7458. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemloc 7451* | Lemma for caucvgpr 7458. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemcl 7452* | Lemma for caucvgpr 7458. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
Theorem | caucvgprlemladdfu 7453* | Lemma for caucvgpr 7458. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemladdrl 7454* | Lemma for caucvgpr 7458. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.) |
Theorem | caucvgprlem1 7455* | Lemma for caucvgpr 7458. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlem2 7456* | Lemma for caucvgpr 7458. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlemlim 7457* | Lemma for caucvgpr 7458. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
Theorem | caucvgpr 7458* |
A Cauchy sequence of positive fractions with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
of the nth term (it should later be able
to prove versions
of this theorem with a different fixed rate or a modulus of
convergence supplied as a hypothesis). We also specify that every
term needs to be larger than a fraction , to avoid the case
where we have positive terms which "converge" to zero (which
is not a
positive real).
This proof (including its lemmas) is similar to the proofs of cauappcvgpr 7438 and caucvgprpr 7488. Reading cauappcvgpr 7438 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) |
Theorem | caucvgprprlemk 7459* | Lemma for caucvgprpr 7488. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) |
Theorem | caucvgprprlemloccalc 7460* | Lemma for caucvgprpr 7488. Rearranging some expressions for caucvgprprlemloc 7479. (Contributed by Jim Kingdon, 8-Feb-2021.) |
Theorem | caucvgprprlemell 7461* | Lemma for caucvgprpr 7488. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) |
Theorem | caucvgprprlemelu 7462* | Lemma for caucvgprpr 7488. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) |
Theorem | caucvgprprlemcbv 7463* | Lemma for caucvgprpr 7488. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemval 7464* | Lemma for caucvgprpr 7488. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) |
Theorem | caucvgprprlemnkltj 7465* | Lemma for caucvgprpr 7488. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkeqj 7466* | Lemma for caucvgprpr 7488. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnjltk 7467* | Lemma for caucvgprpr 7488. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkj 7468* | Lemma for caucvgprpr 7488. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) |
Theorem | caucvgprprlemnbj 7469* | Lemma for caucvgprpr 7488. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.) |
Theorem | caucvgprprlemml 7470* | Lemma for caucvgprpr 7488. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
Theorem | caucvgprprlemmu 7471* | Lemma for caucvgprpr 7488. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
Theorem | caucvgprprlemm 7472* | Lemma for caucvgprpr 7488. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemopl 7473* | Lemma for caucvgprpr 7488. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemlol 7474* | Lemma for caucvgprpr 7488. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemopu 7475* | Lemma for caucvgprpr 7488. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemupu 7476* | Lemma for caucvgprpr 7488. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemrnd 7477* | Lemma for caucvgprpr 7488. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemdisj 7478* | Lemma for caucvgprpr 7488. The putative limit is disjoint. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemloc 7479* | Lemma for caucvgprpr 7488. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemcl 7480* | Lemma for caucvgprpr 7488. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-2020.) |
Theorem | caucvgprprlemclphr 7481* | Lemma for caucvgprpr 7488. The putative limit is a positive real. Like caucvgprprlemcl 7480 but without a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Jun-2021.) |
Theorem | caucvgprprlemexbt 7482* | Lemma for caucvgprpr 7488. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-Jun-2021.) |
Theorem | caucvgprprlemexb 7483* | Lemma for caucvgprpr 7488. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-Jun-2021.) |
Theorem | caucvgprprlemaddq 7484* | Lemma for caucvgprpr 7488. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-Jun-2021.) |
Theorem | caucvgprprlem1 7485* | Lemma for caucvgprpr 7488. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprprlem2 7486* | Lemma for caucvgprpr 7488. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprprlemlim 7487* | Lemma for caucvgprpr 7488. The putative limit is a limit. (Contributed by Jim Kingdon, 21-Nov-2020.) |
Theorem | caucvgprpr 7488* |
A Cauchy sequence of positive reals with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
of the nth term (it should later be able
to prove versions
of this theorem with a different fixed rate or a modulus of
convergence supplied as a hypothesis). We also specify that every
term needs to be larger than a given value , to avoid the case
where we have positive terms which "converge" to zero (which
is not a
positive real).
This is similar to caucvgpr 7458 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 7438) might help in understanding this one, as they are slightly simpler but similarly structured. (Contributed by Jim Kingdon, 14-Nov-2020.) |
Theorem | suplocexprlemell 7489* | Lemma for suplocexpr 7501. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
Theorem | suplocexprlem2b 7490 | Lemma for suplocexpr 7501. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
Theorem | suplocexprlemss 7491* | Lemma for suplocexpr 7501. is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.) |
Theorem | suplocexprlemml 7492* | Lemma for suplocexpr 7501. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
Theorem | suplocexprlemrl 7493* | Lemma for suplocexpr 7501. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
Theorem | suplocexprlemmu 7494* | Lemma for suplocexpr 7501. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
Theorem | suplocexprlemru 7495* | Lemma for suplocexpr 7501. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
Theorem | suplocexprlemdisj 7496* | Lemma for suplocexpr 7501. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.) |
Theorem | suplocexprlemloc 7497* | Lemma for suplocexpr 7501. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.) |
Theorem | suplocexprlemex 7498* | Lemma for suplocexpr 7501. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.) |
Theorem | suplocexprlemub 7499* | Lemma for suplocexpr 7501. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
Theorem | suplocexprlemlub 7500* | Lemma for suplocexpr 7501. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |