Home | Intuitionistic Logic Explorer Theorem List (p. 136 of 137) | < 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 | setindf 13501* | Axiom of set-induction with a disjoint variable condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.) |
Theorem | setindis 13502* | Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) |
Axiom | ax-bdsetind 13503* | Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.) |
BOUNDED | ||
Theorem | bdsetindis 13504* | Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bj-inf2vnlem1 13505* | Lemma for bj-inf2vn 13509. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
Ind | ||
Theorem | bj-inf2vnlem2 13506* | Lemma for bj-inf2vnlem3 13507 and bj-inf2vnlem4 13508. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
Ind | ||
Theorem | bj-inf2vnlem3 13507* | Lemma for bj-inf2vn 13509. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
BOUNDED BOUNDED Ind | ||
Theorem | bj-inf2vnlem4 13508* | Lemma for bj-inf2vn2 13510. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
Ind | ||
Theorem | bj-inf2vn 13509* | A sufficient condition for to be a set. See bj-inf2vn2 13510 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
Theorem | bj-inf2vn2 13510* | A sufficient condition for to be a set; unbounded version of bj-inf2vn 13509. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
Axiom | ax-inf2 13511* | Another axiom of infinity in a constructive setting (see ax-infvn 13476). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.) |
Theorem | bj-omex2 13512 | Using bounded set induction and the strong axiom of infinity, is a set, that is, we recover ax-infvn 13476 (see bj-2inf 13473 for the equivalence of the latter with bj-omex 13477). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | bj-nn0sucALT 13513* | Alternate proof of bj-nn0suc 13499, also constructive but from ax-inf2 13511, hence requiring ax-bdsetind 13503. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
In this section, using the axiom of set induction, we prove full induction on the set of natural numbers. | ||
Theorem | bj-findis 13514* | Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 13482 for a bounded version not requiring ax-setind 4494. See finds 4557 for a proof in IZF. From this version, it is easy to prove of finds 4557, finds2 4558, finds1 4559. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.) |
Theorem | bj-findisg 13515* | Version of bj-findis 13514 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 13514 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
Theorem | bj-findes 13516 | Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 13514 for explanations. From this version, it is easy to prove findes 4560. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
In this section, we state the axiom scheme of strong collection, which is part of CZF set theory. | ||
Axiom | ax-strcoll 13517* | Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that represents a multivalued function on , or equivalently a collection of nonempty classes indexed by , and the axiom asserts the existence of a set which "collects" at least one element in the image of each and which is made only of such elements. That second conjunct is what makes it "strong", compared to the axiom scheme of collection ax-coll 4079. (Contributed by BJ, 5-Oct-2019.) |
Theorem | strcoll2 13518* | Version of ax-strcoll 13517 with one disjoint variable condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.) |
Theorem | strcollnft 13519* | Closed form of strcollnf 13520. (Contributed by BJ, 21-Oct-2019.) |
Theorem | strcollnf 13520* |
Version of ax-strcoll 13517 with one disjoint variable condition
removed,
the other disjoint variable condition replaced with a non-freeness
hypothesis, and without initial universal quantifier. Version of
strcoll2 13518 with the disjoint variable condition on replaced
with a non-freeness hypothesis.
This proof aims to demonstrate a standard technique, but strcoll2 13518 will generally suffice: since the theorem asserts the existence of a set , supposing that that setvar does not occur in the already defined is not a big constraint. (Contributed by BJ, 21-Oct-2019.) |
Theorem | strcollnfALT 13521* | Alternate proof of strcollnf 13520, not using strcollnft 13519. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
In this section, we state the axiom scheme of subset collection, which is part of CZF set theory. | ||
Axiom | ax-sscoll 13522* | Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that represents a multivalued function from to , or equivalently a collection of nonempty subsets of indexed by , and the consequent asserts the existence of a subset of which "collects" at least one element in the image of each and which is made only of such elements. The axiom asserts the existence, for any sets , of a set such that that implication holds for any value of the parameter of . (Contributed by BJ, 5-Oct-2019.) |
Theorem | sscoll2 13523* | Version of ax-sscoll 13522 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.) |
Axiom | ax-ddkcomp 13524 | Axiom of Dedekind completeness for Dedekind real numbers: every inhabited upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then Axiom ax-ddkcomp 13524 should be used in place of construction specific results. In particular, axcaucvg 7803 should be proved from it. (Contributed by BJ, 24-Oct-2021.) |
Theorem | el2oss1o 13525 | Being an element of ordinal two implies being a subset of ordinal one. The converse is equivalent to excluded middle by ss1oel2o 13526. (Contributed by Jim Kingdon, 8-Aug-2022.) |
Theorem | ss1oel2o 13526 | Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4158 which more directly illustrates the contrast with el2oss1o 13525. (Contributed by Jim Kingdon, 8-Aug-2022.) |
EXMID | ||
Theorem | nnti 13527 | Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.) |
Theorem | 012of 13528 | Mapping zero and one between and style integers. (Contributed by Jim Kingdon, 28-Jun-2024.) |
frec | ||
Theorem | 2o01f 13529 | Mapping zero and one between and style integers. (Contributed by Jim Kingdon, 28-Jun-2024.) |
frec | ||
Theorem | pwtrufal 13530 | A subset of the singleton cannot be anything other than or . Removing the double negation would change the meaning, as seen at exmid01 4158. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4156), 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.) |
Theorem | pwle2 13531* | 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.) |
Theorem | pwf1oexmid 13532* | 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 | ||
Theorem | exmid1stab 13533* | 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 | ||
Theorem | subctctexmid 13534* | 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 | ||
Theorem | sssneq 13535* | Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.) |
Theorem | pw1nct 13536* | A condition which ensures that the powerset of a singleton is not countable. The antecedent here can be referred to as the uniformity principle. Based on Mastodon posts by Andrej Bauer and Rahul Chhabra. (Contributed by Jim Kingdon, 29-May-2024.) |
⊔ | ||
Theorem | 0nninf 13537 | The zero element of ℕ∞ (the constant sequence equal to ). (Contributed by Jim Kingdon, 14-Jul-2022.) |
ℕ∞ | ||
Theorem | nninff 13538 | An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
Theorem | nnsf 13539* | Domain and range of . Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
Theorem | peano4nninf 13540* | The successor function on ℕ∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
Theorem | peano3nninf 13541* | The successor function on ℕ∞ is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfalllemn 13542* | Lemma for nninfall 13544. Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
Theorem | nninfalllem1 13543* | Lemma for nninfall 13544. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfall 13544* | 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.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfsellemdc 13545* | Lemma for nninfself 13548. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.) |
ℕ∞ DECID | ||
Theorem | nninfsellemcl 13546* | Lemma for nninfself 13548. (Contributed by Jim Kingdon, 8-Aug-2022.) |
ℕ∞ | ||
Theorem | nninfsellemsuc 13547* | Lemma for nninfself 13548. (Contributed by Jim Kingdon, 6-Aug-2022.) |
ℕ∞ | ||
Theorem | nninfself 13548* | Domain and range of the selection function for ℕ∞. (Contributed by Jim Kingdon, 6-Aug-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
Theorem | nninfsellemeq 13549* | Lemma for nninfsel 13552. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfsellemqall 13550* | Lemma for nninfsel 13552. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfsellemeqinf 13551* | Lemma for nninfsel 13552. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
Theorem | nninfsel 13552* | is a selection function for ℕ∞. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ ℕ∞ | ||
Theorem | nninfomnilem 13553* | Lemma for nninfomni 13554. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ ℕ∞ Omni | ||
Theorem | nninfomni 13554 | ℕ∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ Omni | ||
Theorem | nninffeq 13555* | Equality of two functions on ℕ∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. Remark: the last two hypotheses can be grouped into one, . (Contributed by Jim Kingdon, 4-Aug-2023.) |
ℕ∞ ℕ∞ | ||
Theorem | exmidsbthrlem 13556* | Lemma for exmidsbthr 13557. (Contributed by Jim Kingdon, 11-Aug-2022.) |
ℕ∞ EXMID | ||
Theorem | exmidsbthr 13557* | The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.) |
EXMID | ||
Theorem | exmidsbth 13558* |
The Schroeder-Bernstein Theorem is equivalent to excluded middle. This
is Metamath 100 proof #25. The forward direction (isbth 6904) 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 6904.
The reverse direction (exmidsbthr 13557) 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 | ||
Theorem | sbthomlem 13559 | Lemma for sbthom 13560. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.) |
Omni ⊔ | ||
Theorem | sbthom 13560 | Schroeder-Bernstein is not possible even for . We know by exmidsbth 13558 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 | ||
Theorem | qdencn 13561* | The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 11084 (and also would hold for with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.) |
Theorem | refeq 13562* | 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.) |
Theorem | triap 13563 | Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.) |
DECID # | ||
Theorem | isomninnlem 13564* | Lemma for isomninn 13565. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.) |
frec Omni | ||
Theorem | isomninn 13565* | Omniscience stated in terms of natural numbers. Similar to isomnimap 7063 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 30-Aug-2023.) |
Omni | ||
Theorem | cvgcmp2nlemabs 13566* | Lemma for cvgcmp2n 13567. 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.) |
Theorem | cvgcmp2n 13567* | A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.) |
Theorem | iooref1o 13568 | A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.) |
Theorem | iooreen 13569 | An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.) |
Omniscience principles refer to several propositions, most of them weaker than full excluded middle, which do not follow from the axioms of IZF set theory. They are: (0) the Principle of Omniscience (PO), which is another name for excluded middle (see exmidomni 7068), (1) the Limited Principle of Omniscience (LPO) is Omni (see df-omni 7061), (2) the Weak Limited Principle of Omniscience (WLPO) is WOmni (see df-womni 7090), (3) Markov's Principle (MP) is Markov (see df-markov 7078), (4) the Lesser Limited Principle of Omniscience (LLPO) is not yet defined in iset.mm. They also have analytic counterparts each of which follows from the corresponding omniscience principle: (1) Analytic LPO is real number trichotomy, (see trilpo 13577), (2) Analytic WLPO is decidability of real number equality, DECID (see redcwlpo 13589), (3) Analytic MP is # (see neapmkv 13601), (4) Analytic LLPO is real number dichotomy, (most relevant current theorem is maxclpr 11104). | ||
Theorem | trilpolemclim 13570* | Lemma for trilpo 13577. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.) |
Theorem | trilpolemcl 13571* | Lemma for trilpo 13577. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Theorem | trilpolemisumle 13572* | Lemma for trilpo 13577. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.) |
Theorem | trilpolemgt1 13573* | Lemma for trilpo 13577. The case. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Theorem | trilpolemeq1 13574* | Lemma for trilpo 13577. 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.) |
Theorem | trilpolemlt1 13575* | Lemma for trilpo 13577. 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 7066 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.) |
Theorem | trilpolemres 13576* | Lemma for trilpo 13577. The result. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Theorem | trilpo 13577* |
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 13575 (which means the sequence contains a zero), trilpolemeq1 13574 (which means the sequence is all ones), and trilpolemgt1 13573 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 13563) or that the real numbers are a discrete field (see trirec0 13578). LPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qtri3or 10124 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Omni | ||
Theorem | trirec0 13578* |
Every real number having a reciprocal or equaling zero is equivalent to
real number trichotomy.
This is the key part of the definition of what is known as a discrete field, so "the real numbers are a discrete field" can be taken as an equivalent way to state real trichotomy (see further discussion at trilpo 13577). (Contributed by Jim Kingdon, 10-Jun-2024.) |
Theorem | trirec0xor 13579* |
Version of trirec0 13578 with exclusive-or.
The definition of a discrete field is sometimes stated in terms of exclusive-or but as proved here, this is equivalent to inclusive-or because the two disjuncts cannot be simultaneously true. (Contributed by Jim Kingdon, 10-Jun-2024.) |
Theorem | apdifflemf 13580 | Lemma for apdiff 13582. Being apart from the point halfway between and suffices for to be a different distance from and from . (Contributed by Jim Kingdon, 18-May-2024.) |
# # | ||
Theorem | apdifflemr 13581 | Lemma for apdiff 13582. (Contributed by Jim Kingdon, 19-May-2024.) |
# # # | ||
Theorem | apdiff 13582* | The irrationals (reals apart from any rational) are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 17-May-2024.) |
# # | ||
Theorem | iswomninnlem 13583* | Lemma for iswomnimap 7092. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.) |
frec WOmni DECID | ||
Theorem | iswomninn 13584* | Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7092 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni DECID | ||
Theorem | iswomni0 13585* | Weak omniscience stated in terms of equality with . Like iswomninn 13584 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.) |
WOmni DECID | ||
Theorem | ismkvnnlem 13586* | Lemma for ismkvnn 13587. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
frec Markov | ||
Theorem | ismkvnn 13587* | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.) |
Markov | ||
Theorem | redcwlpolemeq1 13588* | Lemma for redcwlpo 13589. A biconditionalized version of trilpolemeq1 13574. (Contributed by Jim Kingdon, 21-Jun-2024.) |
Theorem | redcwlpo 13589* |
Decidability of real number equality implies the Weak Limited Principle
of Omniscience (WLPO). 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 is all ones or it is not. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. This real number will equal one if and only if the sequence is all ones (redcwlpolemeq1 13588). Therefore decidability of real number equality would imply decidability of whether the sequence is all ones. Because of this theorem, decidability of real number equality is sometimes called "analytic WLPO". WLPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qdceq 10128 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.) |
DECID WOmni | ||
Theorem | tridceq 13590* | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 13577 and redcwlpo 13589). Thus, this is an analytic analogue to lpowlpo 7094. (Contributed by Jim Kingdon, 24-Jul-2024.) |
DECID | ||
Theorem | redc0 13591* | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) |
DECID DECID | ||
Theorem | reap0 13592* | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) |
DECID # | ||
Theorem | dceqnconst 13593* | Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 13589 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.) |
DECID | ||
Theorem | dcapnconst 13594* |
Decidability of real number apartness implies the existence of a certain
non-constant function from real numbers to integers. Variation of
Exercise 11.6(i) of [HoTT], p. (varies).
See trilpo 13577 for more
discussion of decidability of real number apartness.
This is a weaker form of dceqnconst 13593 and in fact this theorem can be proved using dceqnconst 13593 as shown at dcapnconstALT 13595. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) |
DECID # | ||
Theorem | dcapnconstALT 13595* | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 13594 by means of dceqnconst 13593. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
DECID # | ||
Theorem | nconstwlpolem0 13596* | Lemma for nconstwlpo 13599. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
Theorem | nconstwlpolemgt0 13597* | Lemma for nconstwlpo 13599. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
Theorem | nconstwlpolem 13598* | Lemma for nconstwlpo 13599. (Contributed by Jim Kingdon, 23-Jul-2024.) |
Theorem | nconstwlpo 13599* | Existence of a certain non-constant function from reals to integers implies WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.) |
WOmni | ||
Theorem | neapmkvlem 13600* | Lemma for neapmkv 13601. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
# |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |