Home | Intuitionistic Logic Explorer Theorem List (p. 65 of 108) | < 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 | supeq1i 6401 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | supeq2 6402 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | supeq3 6403 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
Theorem | supeq123d 6404 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
Theorem | nfsup 6405 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
Theorem | supmoti 6406* | Any class has at most one supremum in (where is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 7191) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.) |
Theorem | supeuti 6407* | A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by Jim Kingdon, 23-Nov-2021.) |
Theorem | supval2ti 6408* | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
Theorem | eqsupti 6409* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
Theorem | eqsuptid 6410* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | supclti 6411* | A supremum belongs to its base class (closure law). See also supubti 6412 and suplubti 6413. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | supubti 6412* |
A supremum is an upper bound. See also supclti 6411 and suplubti 6413.
This proof demonstrates how to expand an iota-based definition (df-iota 4887) using riotacl2 5501. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | suplubti 6413* | A supremum is the least upper bound. See also supclti 6411 and supubti 6412. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | suplub2ti 6414* | Bidirectional form of suplubti 6413. (Contributed by Jim Kingdon, 17-Jan-2022.) |
Theorem | supelti 6415* | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
Theorem | sup00 6416 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
Theorem | supmaxti 6417* | The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jim Kingdon, 24-Nov-2021.) |
Theorem | supsnti 6418* | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
Theorem | isotilem 6419* | Lemma for isoti 6420. (Contributed by Jim Kingdon, 26-Nov-2021.) |
Theorem | isoti 6420* | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
Theorem | supisolem 6421* | Lemma for supisoti 6423. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | supisoex 6422* | Lemma for supisoti 6423. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | supisoti 6423* | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
Theorem | infeq1 6424 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq1d 6425 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq1i 6426 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq2 6427 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq3 6428 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | infeq123d 6429 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
inf inf | ||
Theorem | nfinf 6430 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
inf | ||
Theorem | cnvinfex 6431* | Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.) |
Theorem | cnvti 6432* | If a relation satisfies a condition corresponding to tightness of an apartness generated by an order, so does its converse. (Contributed by Jim Kingdon, 17-Dec-2021.) |
Theorem | eqinfti 6433* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
inf | ||
Theorem | eqinftid 6434* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
inf | ||
Theorem | infvalti 6435* | Alternate expression for the infimum. (Contributed by Jim Kingdon, 17-Dec-2021.) |
inf | ||
Theorem | infclti 6436* | An infimum belongs to its base class (closure law). See also inflbti 6437 and infglbti 6438. (Contributed by Jim Kingdon, 17-Dec-2021.) |
inf | ||
Theorem | inflbti 6437* | An infimum is a lower bound. See also infclti 6436 and infglbti 6438. (Contributed by Jim Kingdon, 18-Dec-2021.) |
inf | ||
Theorem | infglbti 6438* | An infimum is the greatest lower bound. See also infclti 6436 and inflbti 6437. (Contributed by Jim Kingdon, 18-Dec-2021.) |
inf | ||
Theorem | infnlbti 6439* | A lower bound is not greater than the infimum. (Contributed by Jim Kingdon, 18-Dec-2021.) |
inf | ||
Theorem | infminti 6440* | The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by Jim Kingdon, 18-Dec-2021.) |
inf | ||
Theorem | infmoti 6441* | Any class has at most one infimum in (where is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.) |
Theorem | infeuti 6442* | An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.) |
Theorem | infsnti 6443* | The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.) |
inf | ||
Theorem | inf00 6444 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
inf | ||
Theorem | infisoti 6445* | Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.) |
inf inf | ||
Theorem | ordiso2 6446 | Generalize ordiso 6447 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
Theorem | ordiso 6447* | Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009.) (Proof shortened by Mario Carneiro, 24-Jun-2015.) |
Syntax | ccrd 6448 | Extend class definition to include the cardinal size function. |
Definition | df-card 6449* | Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003.) |
Theorem | cardcl 6450* | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | isnumi 6451 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | finnum 6452 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
Theorem | onenon 6453 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Theorem | cardval3ex 6454* | The value of . (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | oncardval 6455* | The value of the cardinal number function with an ordinal number as its argument. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.) |
Theorem | cardonle 6456 | The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85. (Contributed by NM, 22-Oct-2003.) |
Theorem | card0 6457 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
Theorem | carden2bex 6458* | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
Theorem | pm54.43 6459 | Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.) |
Theorem | pr2nelem 6460 | Lemma for pr2ne 6461. (Contributed by FL, 17-Aug-2008.) |
Theorem | pr2ne 6461 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
This section derives the basics of real and complex numbers. To construct the real numbers constructively, we follow two main sources. The first is Metamath Proof Explorer, which has the advantage of being already formalized in metamath. Its disadvantage, for our purposes, is that it assumes the law of the excluded middle throughout. Since we have already developed natural numbers ( for example, nna0 6076 and similar theorems ), going from there to positive integers (df-ni 6494) and then positive rational numbers (df-nqqs 6538) does not involve a major change in approach compared with the Metamath Proof Explorer. It is when we proceed to Dedekind cuts that we bring in more material from Section 11.2 of [HoTT], which focuses on the aspects of Dedekind cuts which are different without excluded middle. With excluded middle, it is natural to define the cut as the lower set only (as Metamath Proof Explorer does), but we define the cut as a pair of both the lower and upper sets, as [HoTT] does. There are also differences in how we handle order and replacing "not equal to zero" with "apart from zero". | ||
Syntax | cnpi 6462 |
The set of positive integers, which is the set of natural numbers
with 0 removed.
Note: This is the start of the Dedekind-cut construction of real and _complex numbers. |
Syntax | cpli 6463 | Positive integer addition. |
Syntax | cmi 6464 | Positive integer multiplication. |
Syntax | clti 6465 | Positive integer ordering relation. |
Syntax | cplpq 6466 | Positive pre-fraction addition. |
Syntax | cmpq 6467 | Positive pre-fraction multiplication. |
Syntax | cltpq 6468 | Positive pre-fraction ordering relation. |
Syntax | ceq 6469 | Equivalence class used to construct positive fractions. |
Syntax | cnq 6470 | Set of positive fractions. |
Syntax | c1q 6471 | The positive fraction constant 1. |
Syntax | cplq 6472 | Positive fraction addition. |
Syntax | cmq 6473 | Positive fraction multiplication. |
Syntax | crq 6474 | Positive fraction reciprocal operation. |
Syntax | cltq 6475 | Positive fraction ordering relation. |
Syntax | ceq0 6476 | Equivalence class used to construct non-negative fractions. |
~Q0 | ||
Syntax | cnq0 6477 | Set of non-negative fractions. |
Q0 | ||
Syntax | c0q0 6478 | The non-negative fraction constant 0. |
0Q0 | ||
Syntax | cplq0 6479 | Non-negative fraction addition. |
+Q0 | ||
Syntax | cmq0 6480 | Non-negative fraction multiplication. |
·Q0 | ||
Syntax | cnp 6481 | Set of positive reals. |
Syntax | c1p 6482 | Positive real constant 1. |
Syntax | cpp 6483 | Positive real addition. |
Syntax | cmp 6484 | Positive real multiplication. |
Syntax | cltp 6485 | Positive real ordering relation. |
Syntax | cer 6486 | Equivalence class used to construct signed reals. |
Syntax | cnr 6487 | Set of signed reals. |
Syntax | c0r 6488 | The signed real constant 0. |
Syntax | c1r 6489 | The signed real constant 1. |
Syntax | cm1r 6490 | The signed real constant -1. |
Syntax | cplr 6491 | Signed real addition. |
Syntax | cmr 6492 | Signed real multiplication. |
Syntax | cltr 6493 | Signed real ordering relation. |
Definition | df-ni 6494 | Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) |
Definition | df-pli 6495 | Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) |
Definition | df-mi 6496 | Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) |
Definition | df-lti 6497 | Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) |
Theorem | elni 6498 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) |
Theorem | pinn 6499 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) |
Theorem | pion 6500 | A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |