Home | Metamath
Proof Explorer Theorem List (p. 385 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clsneircomplex 38401 | The relative complement of the class exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.) |
Theorem | clsneif1o 38402* | If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the operator, then the operator is a one-to-one, onto mapping. (Contributed by RP, 5-Jun-2021.) |
Theorem | clsneicnv 38403* | If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the operator, then the converse of the operator is known. (Contributed by RP, 5-Jun-2021.) |
Theorem | clsneikex 38404* | If closure and neighborhoods functions are related, the closure function exists. (Contributed by RP, 27-Jun-2021.) |
Theorem | clsneinex 38405* | If closure and neighborhoods functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.) |
Theorem | clsneiel1 38406* | If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the operator, then membership in the closure of a subset is equivalent to the complement of the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021.) |
Theorem | clsneiel2 38407* | If a (pseudo-)closure function and a (pseudo-)neighborhood function are related by the operator, then membership in the closure of the complement of a subset is equivalent to the subset not being a neighborhood of the point. (Contributed by RP, 7-Jun-2021.) |
Theorem | clsneifv3 38408* | Value of the neighborhoods (convergents) in terms of the closure (interior) function. (Contributed by RP, 27-Jun-2021.) |
Theorem | clsneifv4 38409* | Value of the the closure (interior) function in terms of the neighborhoods (convergents) function. (Contributed by RP, 27-Jun-2021.) |
Theorem | neicvgbex 38410 | If (pseudo-)neighborhood and (pseudo-)convergent functions are related by the composite operator, , then the base set exists. (Contributed by RP, 4-Jun-2021.) |
Theorem | neicvgrcomplex 38411 | The relative complement of the class exists as a subset of the base set. (Contributed by RP, 26-Jun-2021.) |
Theorem | neicvgf1o 38412* | If neighborhood and convergent functions are related by operator , it is a one-to-one onto relation. (Contributed by RP, 11-Jun-2021.) |
Theorem | neicvgnvo 38413* | If neighborhood and convergent functions are related by operator , it is its own converse function. (Contributed by RP, 11-Jun-2021.) |
Theorem | neicvgnvor 38414* | If neighborhood and convergent functions are related by operator , the relationship holds with the functions swapped. (Contributed by RP, 11-Jun-2021.) |
Theorem | neicvgmex 38415* | If the neighborhoods and convergents functions are related, the convergents function exists. (Contributed by RP, 27-Jun-2021.) |
Theorem | neicvgnex 38416* | If the neighborhoods and convergents functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021.) |
Theorem | neicvgel1 38417* | A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of that point. (Contributed by RP, 12-Jun-2021.) |
Theorem | neicvgel2 38418* | The complement of a subset being an element of a neighborhood at a point is equivalent to that subset not being a element of the convergent at that point. (Contributed by RP, 12-Jun-2021.) |
Theorem | neicvgfv 38419* | The value of the neighborhoods (convergents) in terms of the the convergents (neighborhoods) function. (Contributed by RP, 27-Jun-2021.) |
Theorem | ntrrn 38420 | The range of the interior function of a topology a subset of the open sets of the topology. (Contributed by RP, 22-Apr-2021.) |
Theorem | ntrf 38421 | The interior function of a topology is a map from the powerset of the base set to the open sets of the topology. (Contributed by RP, 22-Apr-2021.) |
Theorem | ntrf2 38422 | The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.) |
Theorem | ntrelmap 38423 | The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.) |
Theorem | clsf2 38424 | The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 20852. (Contributed by RP, 22-Apr-2021.) |
Theorem | clselmap 38425 | The closure function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021.) |
Theorem | dssmapntrcls 38426* | The interior and closure operators on a topology are duals of each other. See also kur14lem2 31189. (Contributed by RP, 21-Apr-2021.) |
Theorem | dssmapclsntr 38427* | The closure and interior operators on a topology are duals of each other. See also kur14lem2 31189. (Contributed by RP, 22-Apr-2021.) |
Any neighborhood space is an open set topology and any open set topology is a neighborhood space. Seifert And Threlfall define a generic neighborhood space which is a superset of what is now generally used and related concepts and the following will show that those definitions apply to elements of . Seifert And Threlfall do not allow neighborhood spaces on the empty set while sn0top 20803 is an example of a topology with an empty base set. This divergence is unlikely to pose serious problems. | ||
Theorem | gneispa 38428* | Each point of the neighborhood space has at least one neighborhood; each neighborhood of contains . Axiom A of Seifert And Threlfall. (Contributed by RP, 5-Apr-2021.) |
Theorem | gneispb 38429* | Given a neighborhood of , each subset of the neighborhood space containing this neighborhood is also a neighborhood of . Axiom B of Seifert And Threlfall. (Contributed by RP, 5-Apr-2021.) |
Theorem | gneispace2 38430* | The predicate that is a (generic) Seifert And Threlfall neighborhood space. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispace3 38431* | The predicate that is a (generic) Seifert And Threlfall neighborhood space. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispace 38432* | The predicate that is a (generic) Seifert And Threlfall neighborhood space. (Contributed by RP, 14-Apr-2021.) |
Theorem | gneispacef 38433* | A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispacef2 38434* | A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispacefun 38435* | A generic neighborhood space is a function. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispacern 38436* | A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispacern2 38437* | A generic neighborhood space has a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispace0nelrn 38438* | A generic neighborhood space has a non-empty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispace0nelrn2 38439* | A generic neighborhood space has a non-empty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispace0nelrn3 38440* | A generic neighborhood space has a non-empty set of neighborhoods for every point in its domain. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispaceel 38441* | Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispaceel2 38442* | Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispacess 38443* | All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021.) |
Theorem | gneispacess2 38444* | All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021.) |
See https://kerodon.net/ for a work in progress by Jacob Lurie. | ||
See https://kerodon.net/tag/0004 for introduction to the topological simplex of dimension . | ||
Theorem | k0004lem1 38445 | Application of ssin 3835 to range of a function. (Contributed by RP, 1-Apr-2021.) |
Theorem | k0004lem2 38446 | A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021.) |
Theorem | k0004lem3 38447 | When the value of a mapping on a singleton is known, the mapping is a a completely known singleton. (Contributed by RP, 2-Apr-2021.) |
Theorem | k0004val 38448* | The topological simplex of dimension is the set of real vectors where the components are nonnegative and sum to 1. (Contributed by RP, 29-Mar-2021.) |
Theorem | k0004ss1 38449* | The topological simplex of dimension is a subset of the real vectors of dimension . (Contributed by RP, 29-Mar-2021.) |
Theorem | k0004ss2 38450* | The topological simplex of dimension is a subset of the base set of a real vector space of dimension . (Contributed by RP, 29-Mar-2021.) |
ℝ^ | ||
Theorem | k0004ss3 38451* | The topological simplex of dimension is a subset of the base set of Euclidean space of dimension . (Contributed by RP, 29-Mar-2021.) |
𝔼hil | ||
Theorem | k0004val0 38452* | The topological simplex of dimension 0 is a singleton. (Contributed by RP, 2-Apr-2021.) |
Theorem | inductionexd 38453 | Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | wwlemuld 38454 | Natural deduction form of lemul2d 11916. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | leeq1d 38455 | Specialization of breq1d 4663 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | leeq2d 38456 | Specialization of breq2d 4665 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | absmulrposd 38457 | Specialization of absmuld with absidd 14161. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | imadisjld 38458 | Natural dduction form of one side of imadisj 5484. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | imadisjlnd 38459 | Natural deduction form of one negated side of imadisj 5484. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | wnefimgd 38460 | The image of a mapping from A is non empty if A is non empty. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | fco2d 38461 | Natural deduction form of fco2 6059. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | fvco3d 38462 | Natural deduction form of fvco3 6275. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | wfximgfd 38463 | The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | extoimad 38464* | If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | imo72b2lem0 38465* | Lemma for imo72b2 38475. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | suprleubrd 38466* | Natural deduction form of specialized suprleub 10989. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | imo72b2lem2 38467* | Lemma for imo72b2 38475. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | syldbl2 38468 | Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | funfvima2d 38469 | A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | suprlubrd 38470* | Natural deduction form of specialized suprlub 10987. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | imo72b2lem1 38471* | Lemma for imo72b2 38475. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | lemuldiv3d 38472 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | lemuldiv4d 38473 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | rspcdvinvd 38474* | If something is true for all then it's true for some class. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | imo72b2 38475* | IMO 1972 B2. (14th International Mathemahics Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.) |
This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 10041 1red 10055 readdcld 10069 remulcld 10070 eqcomd 2628. | ||
Theorem | int-addcomd 38476 | AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-addassocd 38477 | AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-addsimpd 38478 | AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-mulcomd 38479 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-mulassocd 38480 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-mulsimpd 38481 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-leftdistd 38482 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-rightdistd 38483 | AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-sqdefd 38484 | SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-mul11d 38485 | First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-mul12d 38486 | Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-add01d 38487 | First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-add02d 38488 | Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-sqgeq0d 38489 | SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-eqprincd 38490 | PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-eqtransd 38491 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-eqmvtd 38492 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-eqineqd 38493 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-ineqmvtd 38494 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-ineq1stprincd 38495 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-ineq2ndprincd 38496 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | int-ineqtransd 38497 | InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 11512 addcomli 10228 00id 10211 addid1i 10223 addid2i 10224 eqid 2622 dec0h 11522 decadd 11570 decaddc 11572. | ||
Theorem | unitadd 38498 | Theorem used in conjunction with decaddc 11572 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
Theorem | gsumws3 38499 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
g | ||
Theorem | gsumws4 38500 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
g |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |