Home | Intuitionistic Logic Explorer Theorem List (p. 69 of 106) | < 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 | cauappcvgprlemm 6801* | Lemma for cauappcvgpr 6818. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemopl 6802* | Lemma for cauappcvgpr 6818. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemlol 6803* | Lemma for cauappcvgpr 6818. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemopu 6804* | Lemma for cauappcvgpr 6818. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemupu 6805* | Lemma for cauappcvgpr 6818. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
Theorem | cauappcvgprlemrnd 6806* | Lemma for cauappcvgpr 6818. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemdisj 6807* | Lemma for cauappcvgpr 6818. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemloc 6808* | Lemma for cauappcvgpr 6818. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
Theorem | cauappcvgprlemcl 6809* | Lemma for cauappcvgpr 6818. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgprlemladdfu 6810* | Lemma for cauappcvgprlemladd 6814. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdfl 6811* | Lemma for cauappcvgprlemladd 6814. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdru 6812* | Lemma for cauappcvgprlemladd 6814. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladdrl 6813* | Lemma for cauappcvgprlemladd 6814. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
Theorem | cauappcvgprlemladd 6814* | Lemma for cauappcvgpr 6818. This takes and offsets it by the positive fraction . (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem1 6815* | Lemma for cauappcvgpr 6818. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlem2 6816* | Lemma for cauappcvgpr 6818. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
Theorem | cauappcvgprlemlim 6817* | Lemma for cauappcvgpr 6818. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
Theorem | cauappcvgpr 6818* |
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 6838 and caucvgprpr 6868 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) |
Theorem | archrecnq 6819* | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | archrecpr 6820* | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprlemk 6821 | Lemma for caucvgpr 6838. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemnkj 6822* | Lemma for caucvgpr 6838. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
Theorem | caucvgprlemnbj 6823* | Lemma for caucvgpr 6838. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
Theorem | caucvgprlemm 6824* | Lemma for caucvgpr 6838. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemopl 6825* | Lemma for caucvgpr 6838. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemlol 6826* | Lemma for caucvgpr 6838. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemopu 6827* | Lemma for caucvgpr 6838. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemupu 6828* | Lemma for caucvgpr 6838. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
Theorem | caucvgprlemrnd 6829* | Lemma for caucvgpr 6838. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemdisj 6830* | Lemma for caucvgpr 6838. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemloc 6831* | Lemma for caucvgpr 6838. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
Theorem | caucvgprlemcl 6832* | Lemma for caucvgpr 6838. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
Theorem | caucvgprlemladdfu 6833* | Lemma for caucvgpr 6838. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.) |
Theorem | caucvgprlemladdrl 6834* | Lemma for caucvgpr 6838. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.) |
Theorem | caucvgprlem1 6835* | Lemma for caucvgpr 6838. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlem2 6836* | Lemma for caucvgpr 6838. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
Theorem | caucvgprlemlim 6837* | Lemma for caucvgpr 6838. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
Theorem | caucvgpr 6838* |
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 6818 and caucvgprpr 6868. Reading cauappcvgpr 6818 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) |
Theorem | caucvgprprlemk 6839* | Lemma for caucvgprpr 6868. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) |
Theorem | caucvgprprlemloccalc 6840* | Lemma for caucvgprpr 6868. Rearranging some expressions for caucvgprprlemloc 6859. (Contributed by Jim Kingdon, 8-Feb-2021.) |
Theorem | caucvgprprlemell 6841* | Lemma for caucvgprpr 6868. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) |
Theorem | caucvgprprlemelu 6842* | Lemma for caucvgprpr 6868. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) |
Theorem | caucvgprprlemcbv 6843* | Lemma for caucvgprpr 6868. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemval 6844* | Lemma for caucvgprpr 6868. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) |
Theorem | caucvgprprlemnkltj 6845* | Lemma for caucvgprpr 6868. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkeqj 6846* | Lemma for caucvgprpr 6868. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnjltk 6847* | Lemma for caucvgprpr 6868. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
Theorem | caucvgprprlemnkj 6848* | Lemma for caucvgprpr 6868. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) |
Theorem | caucvgprprlemnbj 6849* | Lemma for caucvgprpr 6868. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.) |
Theorem | caucvgprprlemml 6850* | Lemma for caucvgprpr 6868. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
Theorem | caucvgprprlemmu 6851* | Lemma for caucvgprpr 6868. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
Theorem | caucvgprprlemm 6852* | Lemma for caucvgprpr 6868. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemopl 6853* | Lemma for caucvgprpr 6868. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemlol 6854* | Lemma for caucvgprpr 6868. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemopu 6855* | Lemma for caucvgprpr 6868. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemupu 6856* | Lemma for caucvgprpr 6868. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemrnd 6857* | Lemma for caucvgprpr 6868. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemdisj 6858* | Lemma for caucvgprpr 6868. The putative limit is disjoint. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemloc 6859* | Lemma for caucvgprpr 6868. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.) |
Theorem | caucvgprprlemcl 6860* | Lemma for caucvgprpr 6868. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-2020.) |
Theorem | caucvgprprlemclphr 6861* | Lemma for caucvgprpr 6868. The putative limit is a positive real. Like caucvgprprlemcl 6860 but without a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Jun-2021.) |
Theorem | caucvgprprlemexbt 6862* | Lemma for caucvgprpr 6868. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-Jun-2021.) |
Theorem | caucvgprprlemexb 6863* | Lemma for caucvgprpr 6868. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-Jun-2021.) |
Theorem | caucvgprprlemaddq 6864* | Lemma for caucvgprpr 6868. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-Jun-2021.) |
Theorem | caucvgprprlem1 6865* | Lemma for caucvgprpr 6868. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprprlem2 6866* | Lemma for caucvgprpr 6868. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
Theorem | caucvgprprlemlim 6867* | Lemma for caucvgprpr 6868. The putative limit is a limit. (Contributed by Jim Kingdon, 21-Nov-2020.) |
Theorem | caucvgprpr 6868* |
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 6838 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 6818) might help in understanding this one, as they are slightly simpler but similarly structured. (Contributed by Jim Kingdon, 14-Nov-2020.) |