Home | Metamath
Proof ExplorerTheorem List
(p. 258 of 313)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21423) |
Hilbert Space Explorer
(21424-22946) |
Users' Mathboxes
(22947-31284) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | respreimaOLD 25701 | The preimage of a restricted function. (Moved to respreima 5553 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | foelrnOLD 25702* | Property of a surjective function. (Moved to foelrn 5578 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.) (Contributed by Jeff Madsen, 4-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | foco2OLD 25703 | If a composition of two functions is surjective, then the function on the left is surjective. (Moved to foco2 5579 in main set.mm and may be deleted by mathbox owner, JM. --NM 18-Apr-2013.) (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fnimaprOLD 25704 | The image of a pair under a funtion. (Moved to fnimapr 5482 in main set.mm and may be deleted by mathbox owner, JM. --NM 19-Apr-2013.) (Contributed by Jeff Madsen, 6-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | opelopab3 25705* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |

Theorem | cocanfo 25706 | Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |

Theorem | xpengOLD 25707 | Equinumerosity law for cross product. (Moved to xpen 6957 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fvifOLD 25708 | Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to fvif 5438 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ifeq1daOLD 25709 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifeq1da 3531 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ifeq2daOLD 25710 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifeq2da 3532 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ifcldaOLD 25711 | Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifclda 3533 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | xpeq1dOLD 25712 | Equality deduction for cross product. (Moved to xpeq1d 4665 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | xpeq2dOLD 25713 | Equality deduction for cross product. (Moved to xpeq1d 4665 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | resexOLD 25714 | The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.) (Moved to resex 4948 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | brresi 25715 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | opabex3OLD 25716* | Existence of an ordered pair abstraction. (Moved to opabex3 5668 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Jan-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fnopabeqd 25717* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |

Theorem | fvopabf4g 25718* | Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |

Theorem | eqfnun 25719 | Two functions on are equal if and only if they have equal restrictions to both and . (Contributed by Jeff Madsen, 19-Jun-2011.) |

Theorem | fnopabco 25720* | Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |

Theorem | opropabco 25721* | Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |

Theorem | oprabexdOLD 25722* | Existence of an operator abstraction. (Moved to oprabexd 5859 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | f1opr 25723* | Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.) |

Theorem | cnvcanOLD 25724 | Composition with the converse. (Moved to funcocnv2 5401 in main set.mm and may be deleted by mathbox owner, JM. --NM 28-Feb-2015.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | cocnv 25725 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | f1ocan1fv 25726 | Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |

Theorem | f1ocan2fv 25727 | Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | f1elimaOLD 25728 | Membership in the image of a 1-1 map. (Moved to f1elima 5686 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | enf1f1oOLD 25729 | A one-to-one mapping of finite sets with the same cardinality is bijective. (Moved to f1finf1o 7019 in main set.mm and may be deleted by mathbox owner, JM. --NM 24-Sep-2013.) (Contributed by Jeff Madsen, 5-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | eqfnfv3OLD 25730* | Derive equality of functions from equality of their values. (Moved to eqfnfv3 5523 in main set.mm and may be deleted by mathbox owner, JM. --NM 22-Nov-2011.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | inixp 25731* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | ixpssmapgOLD 25732* | An infinite Cartesian product is a subset of set exponentiation. (Moved into main set.mm as ixpssmapg 6779 and may be deleted by mathbox owner, JM. --NM 18-Jun-2013.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | mapfiOLD 25733 | Set exponentiation of finite sets is finite. (Moved into main set.mm as mapfi 7085 and may be deleted by mathbox owner, JM. --NM 24-Sep-2013.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ixpfiOLD 25734* | A cross product of finitely many finite sets is finite. (Moved into main set.mm as ixpfi 7086 and may be deleted by mathbox owner, JM. --NM 24-Sep-2013.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | upixp 25735* | Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |

Theorem | abrexex2gOLD 25736* | Existence of an existentially restricted class abstraction. (Moved to abrexex2g 5667 in main set.mm and may be deleted by mathbox owner, JM. --NM 21-May-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | abrexdom 25737* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | abrexdom2 25738* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | findcard2OLD 25739* | Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Moved to findcard2 7031 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Nov-2012.) (Contributed by Jeff Madsen, 8-Jul-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fimaxOLD 25740* | A finite set has a maximum under a total order. (Moved to fimaxg 7037 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fimaxgOLD 25741* | A finite set has a maximum under a total order. (Moved to fimaxg 7037 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fisupgOLD 25742* | Lemma showing existence and closure of supremum of a finite set. (Moved to fisupg 7038 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ac6gf 25743* | Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | indexa 25744* | If for every element of an indexing set there exists a corresponding element of another set , then there exists a subset of consisting only of those elements which are indexed by . Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | indexdom 25745* | If for every element of an indexing set there exists a corresponding element of another set , then there exists a subset of consisting only of those elements which are indexed by , and which is dominated by the set . (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | indexfiOLD 25746* | If for every element of a finite indexing set there exists a corresponding element of another set , then there exists a finite subset of consisting only of those elements which are indexed by . Proven without the Axiom of Choice, unlike indexdom 25745. (Moved to indexfi 7096 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Apr-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fipreimaOLD 25747* | Given a finite subset of the range of a function, there exists a finite subset of the domain whose image is . (Moved to fipreima 7094 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Apr-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 1-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | frinfm 25748* | A subset of a well founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | welb 25749* | A non-empty subset of a well ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | supeq2OLD 25750 | Equality theorem for supremum. (Moved to supeq2 7134 in main set.mm and may be deleted by mathbox owner, JM. --NM 24-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | supex2g 25751 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | supclt 25752* | Closure of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | supubt 25753* | Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | infmrlbOLD 25754* | A member of a non-empty bounded set of reals is greater than or equal to the set's lower bound. (Contributed by Jeff Madsen, 2-Feb-2011.) (Moved to infmrlb 9668 in main set.mm and may be deleted by mathbox owner, JM. --NM 21-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | supeutOLD 25755* | A supremum is unique. Closed version of supeu 7138. (Moved to supeu 7138 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 9-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fisup2gOLD 25756 | A nonempty finite set contains its supremum. (Moved to fisupcl 7151 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 9-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fimax2gOLD 25757* | A finite set has a maximum under a total order. (Moved to fimax2g 7036 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | wofiOLD 25758 | A total order on a finite set is a well order. (Moved to wofi 7039 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | frfiOLD 25759 | A partial order is founded on a finite set. (Moved to frfi 7035 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | pofunOLD 25760* | A function preserves a partial order relation. (Moved to pofun 4267 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | frminexOLD 25761* | If an element of a founded set satisfies a property , then there is a minimal element that satisfies . (Moved to frminex 4310 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

16.14.2 Real and complex numbers;
integers | ||

Theorem | fimaxreOLD 25762* | A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to fimaxre 9634 in main set.mm and may be deleted by mathbox owner, JM. --NM 22-Mar-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fimaxre2OLD 25763* | A nonempty finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 27-May-2011.) (Moved to fimaxre2 9635 in main set.mm and may be deleted by mathbox owner, JM. --NM 22-Mar-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | filbcmb 25764* | Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | add20OLD 25765 | Two nonnegative numbers are zero iff their sum is zero. (Moved to add20 9219 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | addsubeq4OLD 25766 | Relation between sums and differences.. (Moved to addsubeq4 8999 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rdr 25767 | Two ways of expressing the remainder when is divided by . (Contributed by Jeff Madsen, 17-Jun-2010.) |

Theorem | eluzaddOLD 25768 | Membership in a later set of upper integers. (Moved to eluzadd 10188 in main set.mm and may be deleted by mathbox owner, JM. --NM 2-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | eluzsubOLD 25769 | Membership in an earlier set of upper integers. (Moved to eluzsub 10189 in main set.mm and may be deleted by mathbox owner, JM. --NM 2-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | uzm1OLD 25770 | Choices for an element of an upper interval of integers. (Moved to uzm1 10190 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-May-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | uzp1OLD 25771 | Choices for an element of an upper interval of integers. (Moved to uzp1 10193 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-May-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fzfiOLD 25772 | A finite interval of integers is finite. (Moved to fzfi 10965 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fzfi2OLD 25773 | Variant of fzfi 10965 with hypothesis weakened. (Moved to fzfi 10965 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 16-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fz10OLD 25774 | There are no integers between 1 and 0. (Moved to fz10 10745 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 16-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fzmul 25775 | Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |

Theorem | fzadd2 25776 | Membership of a sum in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |

Theorem | fzsplitOLD 25777 | Split a finite interval of integers into two parts. (Moved to fzsplit 10747 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fzdisjOLD 25778 | Condition for two finite intervals of integers to be disjoint. (Moved to fzdisj 10748 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fzp1elp1OLD 25779 | Add one to an element of a finite set of integers. (Moved to fzp1elp1 10770 in main set.mm and may be deleted by mathbox owner, JM. --NM 28-Feb-2014.) (Contributed by Jeff Madsen, 6-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | abszOLD 25780 | A real number is an integer iff its absolute value is an integer. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to absz 11726 in main set.mm and may be deleted by mathbox owner, JM. --NM 10-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | mod0OLD 25781 | is zero iff is evenly divisible by . (Moved to mod0 10909 in main set.mm and may be deleted by mathbox owner, JM. --NM 19-Apr-2014.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | negmod0OLD 25782 | is divisible by iff its negative is. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to negmod0 10910 in main set.mm and may be deleted by mathbox owner, JM. --NM 10-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | absmod0OLD 25783 | is divisible by iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to absmod0 11718 in main set.mm and may be deleted by mathbox owner, JM. --NM 10-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

16.14.3 Sequences and sums | ||

Theorem | sdclem2 25784* | Lemma for sdc 25786. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | sdclem1 25785* | Lemma for sdc 25786. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | sdc 25786* | Strong dependent choice. Suppose we may choose an element of such that property holds, and suppose that if we have already chosen the first elements (represented here by a function from to ), we may choose another element so that all elements taken together have property . Then there exists an infinite sequence of elements of such that the first terms of this sequence satisfy for all . This theorem allows us to construct infinite seqeunces where each term depends on all the previous terms in the sequence. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 3-Jun-2014.) |

Theorem | fdc 25787* | Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010.) |

Theorem | fdc1 25788* | Variant of fdc 25787 with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010.) |

Theorem | seqpo 25789* | Two ways to say that a sequence respects a partial order. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | incsequz 25790* | An increasing sequence of natural numbers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | incsequz2 25791* | An increasing sequence of natural numbers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | nnubfi 25792* | A bounded above set of natural numbers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.) |

Theorem | nninfnub 25793* | An infinite set of natural numbers is unbounded above. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.) |

Theorem | csbrn 25794* | Cauchy-Schwarz-Bunjakovsky inequality for R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.) |

Theorem | trirn 25795* | Triangle inequality in R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.) |

16.14.4 Topology | ||

Theorem | unopnOLD 25796 | The union of two open sets is open. (Moved to unopn 16576 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | incldOLD 25797 | The intersection of two closed sets is closed. (Moved to incld 16707 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | subspopn 25798 | An open set is open in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |

↾_{t} | ||

Theorem | neificl 25799 | Neighborhoods are closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Nov-2013.) |

Theorem | lpss2 25800 | Limit points of a subset are limit points of the larger set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |