P. 99 of Theorem List - Intuitionistic Logic Explorer

Home	Intuitionistic Logic Explorer Theorem List (p. 99 of 102)	< Previous Next >
		Browser slow? Try the Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9801-9900 *Has distinct variable group(s)

Type

Label

Description

Statement

Theorem

climrel 9801

The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theorem

clim 9802*

Express the predicate: The limit of complex number sequence

, or

converges to

. This means that for any real

, no matter how small, there always exists an integer

such that the absolute difference of any later complex number in the sequence and the limit is less than

. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

$/\$

Theorem

climcl 9803

Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Theorem

clim2 9804*

Express the predicate: The limit of complex number sequence

, or

converges to

, with more general quantifier restrictions than clim 9802. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

clim2c 9805*

Express the predicate

converges to

. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

clim0 9806*

Express the predicate

converges to

. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

clim0c 9807*

Express the predicate

converges to

. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climi 9808*

Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climi2 9809*

Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climi0 9810*

Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climconst 9811*

An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climconst2 9812

A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climz 9813

The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theorem

climuni 9814

An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

fclim 9815

The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theorem

climdm 9816

Two ways to express that a function has a limit. (The expression

is sometimes useful as a shorthand for "the unique limit of the function

"). (Contributed by Mario Carneiro, 18-Mar-2014.)

Theorem

climeu 9817*

An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)

Theorem

climreu 9818*

An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)

Theorem

climmo 9819*

An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)

Theorem

climeq 9820*

Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climmpt 9821*

Exhibit a function

with the same convergence properties as the not-quite-function

. (Contributed by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

2clim 9822*

If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climshftlemg 9823

A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)

$/\$

Theorem

climres 9824

A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climshft 9825

A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

iserclim0 9826

The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.)

Theorem

climshft2 9827*

A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)

$/\$

Theorem

climabs0 9828*

Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climcn1 9829*

Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climcn2 9830*

Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

addcn2 9831*

Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcn for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

subcn2 9832*

Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

mulcn2 9833*

Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

cn1lem 9834*

A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

abscn2 9835*

The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

cjcn2 9836*

The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

recn2 9837*

The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

imcn2 9838*

The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

climcn1lem 9839*

The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

climabs 9840*

Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

climcj 9841*

Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

climre 9842*

Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

climim 9843*

Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

climrecl 9844*

The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.)

$/\$

Theorem

climge0 9845*

A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.)

$/\$

Theorem

climadd 9846*

Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

$/\$

Theorem

climmul 9847*

Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)

$/\$

Theorem

climsub 9848*

Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)

$/\$

Theorem

climaddc1 9849*

Limit of a constant

added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

$/\$

Theorem

climaddc2 9850*

Limit of a constant

added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

$/\$

Theorem

climmulc2 9851*

Limit of a sequence multiplied by a constant

. Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

$/\$

Theorem

climsubc1 9852*

Limit of a constant

subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

climsubc2 9853*

Limit of a constant

minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)

$/\$

Theorem

climle 9854*

Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)

$/\$

Theorem

climsqz 9855*

Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)

$/\$

Theorem

climsqz2 9856*

Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)

$/\$

Theorem

clim2iser 9857*

The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.)

$/\$

Theorem

clim2iser2 9858*

The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.)

$/\$

Theorem

iiserex 9859*

An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)

$/\$

Theorem

iisermulc2 9860*

Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)

$/\$

Theorem

climlec2 9861*

Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)

$/\$

Theorem

iserile 9862*

Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.)

$/\$

Theorem

iserige0 9863*

The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)

$/\$

Theorem

climub 9864*

The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)

$/\$

Theorem

climserile 9865*

The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.)

$/\$

Theorem

climcau 9866*

A converging sequence of complex numbers is a Cauchy sequence. The converse would require excluded middle or a different definition of Cauchy sequence (for example, fixing a rate of convergence as in climcvg1n 9869). Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.)

$/\$

Theorem

climrecvg1n 9867*

A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within

of the nth term, where

is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)

Theorem

climcvg1nlem 9868*

Lemma for climcvg1n 9869. We construct sequences of the real and imaginary parts of each term of

, show those converge, and use that to show that

converges. (Contributed by Jim Kingdon, 24-Aug-2021.)

Theorem

climcvg1n 9869*

A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within

of the nth term, where

is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)

Theorem

climcaucn 9870*

A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 9866 but adds the part that

is complex. (Contributed by Jim Kingdon, 24-Aug-2021.)

$/\$

Theorem

serif0 9871*

If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.)

$/\$

3.8.2 Finite and infinite sums

Syntax

csu 9872

Extend class notation to include finite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.)

Definition

df-sum 9873*

Define the sum of a series with an index set of integers

is normally a free variable in

, i.e.

can be thought of as

. This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers). Examples:

means

, and

means 1/2 + 1/4 + 1/8 + ... = 1. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

$/\$

$\/$

$/\$

Theorem

sumeq1 9874

Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Theorem

nfsum1 9875

Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Theorem

nfsum 9876

Bound-variable hypothesis builder for sum: if

is (effectively) not free in

and

, it is not free in

. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

PART 4 ELEMENTARY NUMBER THEORY

Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory.

4.1 Elementary properties of divisibility

4.1.1 Rationality of square root of 2

Theorem

sqr2irrlem 9877

Lemma concerning rationality of square root of 2. The core of the proof - if

, then

and

are even, so

and

are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)

$/\$

Theorem

sqrt2irr 9878

The square root of 2 is not rational. That is, for any rational number,

does not equal it. However, if we were to say "the square root of 2 is irrational" that would mean something stronger: "for any rational number,

is apart from it" (the two statements are equivalent given excluded middle). We do not prove irrationality in this stronger sense here.

The proof's core is proven in sqr2irrlem 9877, which shows that if , then and are even, so and are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)

Theorem

sqrt2re 9879

The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.)

4.1.2 Algorithms

Theorem

nn0seqcvgd 9880*

A strictly-decreasing nonnegative integer sequence with initial term

reaches zero by the

th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.)

$/\$

Theorem

ialgrlem1st 9881

Lemma for ialgr0 9883. Expressing algrflemg 5851 in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.)

$/\$

Theorem

ialgrlemconst 9882

Lemma for ialgr0 9883. Closure of a constant function, in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.)

$/\$

Theorem

ialgr0 9883

The value of the algorithm iterator

is the initial state

. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)

Theorem

ialgrf 9884

An algorithm is a step function

on a state space

. An algorithm acts on an initial state

by iteratively applying

to give

and so on. An algorithm is said to halt if a fixed point of

is reached after a finite number of iterations.

The algorithm iterator "runs" the algorithm so that is the state after iterations of on the initial state .

Domain and codomain of the algorithm iterator . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)

Theorem

ialgrp1 9885

The value of the algorithm iterator

. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)

$/\$

Theorem

ialginv 9886*

is an invariant of

, its value is unchanged after any number of iterations of

. (Contributed by Paul Chapman, 31-Mar-2011.)

$/\$

Theorem

ialgcvg 9887*

One way to prove that an algorithm halts is to construct a countdown function

whose value is guaranteed to decrease for each iteration of

until it reaches

. That is, if

is not a fixed point of

, then

If is a countdown function for algorithm , the sequence reaches after at most steps, where is the value of for the initial state . (Contributed by Paul Chapman, 22-Jun-2011.)

Theorem

algcvgblem 9888

Lemma for algcvgb 9889. (Contributed by Paul Chapman, 31-Mar-2011.)

$/\$

Theorem

algcvgb 9889

Two ways of expressing that

is a countdown function for algorithm

. The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011.)

$/\$

Theorem

ialgcvga 9890*

The countdown function

remains

after

steps. (Contributed by Paul Chapman, 22-Jun-2011.)

Theorem

ialgfx 9891*

reaches a fixed point when the countdown function

reaches

remains fixed after

steps. (Contributed by Paul Chapman, 22-Jun-2011.)

PART 5 GUIDES AND MISCELLANEA

5.1 Guides (conventions, explanations, and examples)

5.1.1 Conventions

This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:

Axioms of propositional calculus - Stanford Encyclopedia of Philosophy or [Heyting].
Axioms of predicate calculus - our axioms are adapted from the ones in the Metamath Proof Explorer.
Theorems of propositional calculus - [Heyting].
Theorems of pure predicate calculus - Metamath Proof Explorer.
Theorems of equality and substitution - Metamath Proof Explorer.
Axioms of set theory - [Crosilla].
Development of set theory - Chapter 10 of [HoTT].
Construction of real and complex numbers - Chapter 11 of [HoTT]; [BauerTaylor].
Theorems about real numbers - [Geuvers].

Theorem

conventions 9892

Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (aka "set.mm"). This list of conventions is intended to be read in conjunction with the corresponding conventions in the Metamath Proof Explorer, and only the differences are described below.

Minimizing axioms and the axiom of choice. We prefer proofs that depend on fewer and/or weaker axioms, even if the proofs are longer. In particular, our choice of IZF (Intuitionistic Zermelo-Fraenkel) over CZF (Constructive Zermelo-Fraenkel, a weaker system) was just an expedient choice because IZF is easier to formalize in metamath. You can find some development using CZF in BJ's mathbox starting at ax-bd0 9933 (and the section header just above it). As for the axiom of choice, the full axiom of choice implies excluded middle as seen at acexmid 5511, although some authors will use countable choice or dependent choice. For example, countable choice or excluded middle is needed to show that the Cauchy reals coincide with the Dedekind reals - Corollary 11.4.3 of [HoTT], p. (varies).
Junk/undefined results. Much of the discussion of this topic in the Metamath Proof Explorer applies except that certain techniques are not available to us. For example, the Metamath Proof Explorer will often say "if a function is evaluated within its domain, a certain result follows; if the function is evaluated outside its domain, the same result follows. Since the function must be evaluated within its domain or outside it, the result follows unconditionally" (the use of excluded middle in this argument is perhaps obvious when stated this way). For this reason, we generally need to prove we are evaluating functions within their domains and avoid the reverse closure theorems of the Metamath Proof Explorer.
Bibliography references. The bibliography for the Intuitionistic Logic Explorer is separate from the one for the Metamath Proof Explorer but feel free to copy-paste a citation in either direction in order to cite it.

Label naming conventions

Here are a few of the label naming conventions:

Suffixes. We follow the conventions of the Metamath Proof Explorer with a few additions. A biconditional in set.mm which is an implication in iset.mm should have a "r" (for the reverse direction), or "i"/"im" (for the forward direction) appended. A theorem in set.mm which has a decidability condition added should add "dc" to the theorem name. A theorem in set.mm where "nonempty class" is changed to "inhabited class" should add "m" (for member) to the theorem name.

The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.

Abbreviation	Mnenomic	Source	Expression	Syntax?	Example(s)
ap	apart	df-ap 7573		Yes	apadd1 7599, apne 7614

Community. The Metamath mailing list also covers the Intuitionistic Logic Explorer and is at: https://groups.google.com/forum/#!forum/metamath.

(Contributed by Jim Kingdon, 24-Feb-2020.)

5.1.2 Definitional examples

Theorem

ex-or 9893

Example for ax-io 630. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)

$\/$

Theorem

ex-an 9894

Example for ax-ia1 99. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)

$/\$

Theorem

ex-fl 9895

Example for df-fl 9114. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

$/\$

Theorem

ex-ceil 9896

Example for df-ceil 9115. (Contributed by AV, 4-Sep-2021.)

⌈

$/\$

⌈

PART 6 SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)

6.1 Mathboxes for user contributions

6.1.1 Mathbox guidelines

Theorem

mathbox 9897

(This theorem is a dummy placeholder for these guidelines. The name of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.)

A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm.

For contributors:

By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm.

Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it.

Guidelines:

1. If at all possible, please use only 0-ary class constants for new definitions.

2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website.

3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm.

4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed.

Notes:

1. We may decide to move some theorems to the main part of set.mm for general use.

2. We may make changes to mathboxes to maintain the overall quality of set.mm. Normally we will let you know if a change might impact what you are working on.

3. If you use theorems from another user's mathbox, we don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let us know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)

6.2 Mathbox for Mykola Mostovenko

Theorem

ax1hfs 9898

Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)

$/\$

6.3 Mathbox for BJ

6.3.1 Propositional calculus

Theorem

nnexmid 9899

Double negation of excluded middle. Intuitionistic logic refutes the negation of excluded middle (but, of course, does not prove excluded middle) for any formula. (Contributed by BJ, 9-Oct-2019.)

$\/$

Theorem

nndc 9900

Double negation of decidability of a formula. Intuitionistic logic refutes undecidability (but, of course, does not prove decidability) of any formula. (Contributed by BJ, 9-Oct-2019.)

DECID

< Previous Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124

< Previous Next >