Home | Metamath
Proof Explorer Theorem List (p. 314 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 | cvmlift3lem1 31301* | Lemma for cvmlift3 31310. (Contributed by Mario Carneiro, 6-Jul-2015.) |
CovMap SConn 𝑛Locally PConn | ||
Theorem | cvmlift3lem2 31302* | Lemma for cvmlift2 31298. (Contributed by Mario Carneiro, 6-Jul-2015.) |
CovMap SConn 𝑛Locally PConn | ||
Theorem | cvmlift3lem3 31303* | Lemma for cvmlift2 31298. (Contributed by Mario Carneiro, 6-Jul-2015.) |
CovMap SConn 𝑛Locally PConn | ||
Theorem | cvmlift3lem4 31304* | Lemma for cvmlift2 31298. (Contributed by Mario Carneiro, 6-Jul-2015.) |
CovMap SConn 𝑛Locally PConn | ||
Theorem | cvmlift3lem5 31305* | Lemma for cvmlift2 31298. (Contributed by Mario Carneiro, 6-Jul-2015.) |
CovMap SConn 𝑛Locally PConn | ||
Theorem | cvmlift3lem6 31306* | Lemma for cvmlift3 31310. (Contributed by Mario Carneiro, 9-Jul-2015.) |
CovMap SConn 𝑛Locally PConn ↾t ↾t ↾t | ||
Theorem | cvmlift3lem7 31307* | Lemma for cvmlift3 31310. (Contributed by Mario Carneiro, 9-Jul-2015.) |
CovMap SConn 𝑛Locally PConn ↾t ↾t ↾t PConn | ||
Theorem | cvmlift3lem8 31308* | Lemma for cvmlift2 31298. (Contributed by Mario Carneiro, 6-Jul-2015.) |
CovMap SConn 𝑛Locally PConn ↾t ↾t | ||
Theorem | cvmlift3lem9 31309* | Lemma for cvmlift2 31298. (Contributed by Mario Carneiro, 7-May-2015.) |
CovMap SConn 𝑛Locally PConn ↾t ↾t | ||
Theorem | cvmlift3 31310* | A general version of cvmlift 31281. If is simply connected and weakly locally path-connected, then there is a unique lift of functions on which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015.) |
CovMap SConn 𝑛Locally PConn | ||
Theorem | snmlff 31311* | The function from snmlval 31313 is a mapping from positive integers to real numbers in the range . (Contributed by Mario Carneiro, 6-Apr-2015.) |
Theorem | snmlfval 31312* | The function from snmlval 31313 maps to the relative density of in the first digits of the digit string of in base . (Contributed by Mario Carneiro, 6-Apr-2015.) |
Theorem | snmlval 31313* | The property " is simply normal in base ". A number is simply normal if each digit occurs in the base- digit string of with frequency (which is consistent with the expectation in an infinite random string of numbers selected from ). (Contributed by Mario Carneiro, 6-Apr-2015.) |
Theorem | snmlflim 31314* | If is simply normal, then the function of relative density of in the digit string converges to , i.e. the set of occurrences of in the digit string has natural density . (Contributed by Mario Carneiro, 6-Apr-2015.) |
Syntax | cgoe 31315 | The Godel-set of membership. |
Syntax | cgna 31316 | The Godel-set for the Sheffer stroke. |
Syntax | cgol 31317 | The Godel-set of universal quantification. (Note that this is not a wff.) |
Syntax | csat 31318 | The satisfaction function. |
Syntax | cfmla 31319 | The formula set predicate. |
Syntax | csate 31320 | The -satisfaction function. |
Syntax | cprv 31321 | The "proves" relation. |
Definition | df-goel 31322 | Define the Godel-set of membership. Here the arguments correspond to vN and vP , so actually means v0 v1 , not . (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-gona 31323 | Define the Godel-set for the Sheffer stroke NAND. Here the arguments are also Godel-sets corresponding to smaller formulae. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-goal 31324 | Define the Godel-set of universal quantification. Here corresponds to vN , and represents another formula, and this expression is where is the -th variable, is the code for . Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-sat 31325* |
Define the satisfaction predicate. This recursive construction builds up
a function over wff codes and simultaneously defines the set of
assignments to all variables from that makes the coded wff true in
the model , where is interpreted as the binary relation on .
The interpretation of the statement is that for the model , is a
valuation of the variables (v0 , v1 , etc.) and is a code for a wff using that
is true under the assignment . The function is defined by finite
recursion; only operates on wffs of depth at
most , and operates on all wffs.
The coding scheme for the wffs is defined so that
(Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-sate 31326* | A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable . (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-fmla 31327 | Define the predicate which defines the set of valid Godel formulas. The parameter defines the maximum height of the formulas: the set is all formulas of the form or (which in our coding scheme is the set ; see df-sat 31325 for the full coding scheme), and each extra level adds to the complexity of the formulas in . is the set of all valid formulas. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Syntax | cgon 31328 | The Godel-set of negation. (Note that this is not a wff.) |
Syntax | cgoa 31329 | The Godel-set of conjunction. |
Syntax | cgoi 31330 | The Godel-set of implication. |
Syntax | cgoo 31331 | The Godel-set of disjunction. |
Syntax | cgob 31332 | The Godel-set of equivalence. |
Syntax | cgoq 31333 | The Godel-set of equality. |
Syntax | cgox 31334 | The Godel-set of existential quantification. (Note that this is not a wff.) |
Definition | df-gonot 31335 | Define the Godel-set of negation. Here the argument is also a Godel-set corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-goan 31336* | Define the Godel-set of conjunction. Here the arguments and are also Godel-sets corresponding to smaller formulae. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-goim 31337* | Define the Godel-set of implication. Here the arguments and are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-goor 31338* | Define the Godel-set of disjunction. Here the arguments and are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-gobi 31339* | Define the Godel-set of equivalence. Here the arguments and are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-goeq 31340* | Define the Godel-set of equality. Here the arguments correspond to vN and vP , so actually means v0 v1 , not . Here we use the trick mentioned in ax-ext 2602 to introduce equality as a defined notion in terms of . The expression max here is a convenient way of getting a dummy variable distinct from and . (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-goex 31341 | Define the Godel-set of existential quantification. Here corresponds to vN , and represents another formula, and this expression is where is the -th variable, is the code for . Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-prv 31342* | Define the "proves" relation on a set. A wff is true in a model if for every valuation , the interpretation of the wff using the membership relation on is true. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Syntax | cgze 31343 | The Axiom of Extensionality. |
Syntax | cgzr 31344 | The Axiom Scheme of Replacement. |
Syntax | cgzp 31345 | The Axiom of Power Sets. |
Syntax | cgzu 31346 | The Axiom of Unions. |
Syntax | cgzg 31347 | The Axiom of Regularity. |
Syntax | cgzi 31348 | The Axiom of Infinity. |
Syntax | cgzf 31349 | The set of models of ZF. |
Definition | df-gzext 31350 | The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-gzrep 31351 | The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-gzpow 31352 | The Godel-set version of the Axiom of Power Sets. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-gzun 31353 | The Godel-set version of the Axiom of Unions. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-gzreg 31354 | The Godel-set version of the Axiom of Regularity. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-gzinf 31355 | The Godel-set version of the Axiom of Infinity. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-gzf 31356* | Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013.) |
This is a formalization of Appendix C of the Metamath book, which describes the mathematical representation of a formal system, of which set.mm (this file) is one. | ||
Syntax | cmcn 31357 | The set of constants. |
mCN | ||
Syntax | cmvar 31358 | The set of variables. |
mVR | ||
Syntax | cmty 31359 | The type function. |
mType | ||
Syntax | cmvt 31360 | The set of variable typecodes. |
mVT | ||
Syntax | cmtc 31361 | The set of typecodes. |
mTC | ||
Syntax | cmax 31362 | The set of axioms. |
mAx | ||
Syntax | cmrex 31363 | The set of raw expressions. |
mREx | ||
Syntax | cmex 31364 | The set of expressions. |
mEx | ||
Syntax | cmdv 31365 | The set of distinct variables. |
mDV | ||
Syntax | cmvrs 31366 | The variables in an expression. |
mVars | ||
Syntax | cmrsub 31367 | The set of raw substitutions. |
mRSubst | ||
Syntax | cmsub 31368 | The set of substitutions. |
mSubst | ||
Syntax | cmvh 31369 | The set of variable hypotheses. |
mVH | ||
Syntax | cmpst 31370 | The set of pre-statements. |
mPreSt | ||
Syntax | cmsr 31371 | The reduct of a pre-statement. |
mStRed | ||
Syntax | cmsta 31372 | The set of statements. |
mStat | ||
Syntax | cmfs 31373 | The set of formal systems. |
mFS | ||
Syntax | cmcls 31374 | The closure of a set of statements. |
mCls | ||
Syntax | cmpps 31375 | The set of provable pre-statements. |
mPPSt | ||
Syntax | cmthm 31376 | The set of theorems. |
mThm | ||
Definition | df-mcn 31377 | Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mCN Slot | ||
Definition | df-mvar 31378 | Define the set of variables in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mVR Slot | ||
Definition | df-mty 31379 | Define the type function in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mType Slot | ||
Definition | df-mtc 31380 | Define the set of typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mTC Slot | ||
Definition | df-mmax 31381 | Define the set of axioms in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mAx Slot | ||
Definition | df-mvt 31382 | Define the set of variable typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mVT mType | ||
Definition | df-mrex 31383 | Define the set of "raw expressions", which are expressions without a typecode attached. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mREx Word mCN mVR | ||
Definition | df-mex 31384 | Define the set of expressions, which are strings of constants and variables headed by a typecode constant. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mEx mTC mREx | ||
Definition | df-mdv 31385 | Define the set of distinct variable conditions, which are pairs of distinct variables. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mDV mVR mVR | ||
Definition | df-mvrs 31386* | Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mVars mEx mVR | ||
Definition | df-mrsub 31387* | Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mRSubst mREx mVR mREx freeMndmCN mVR g mCN mVR | ||
Definition | df-msub 31388* | Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mSubst mREx mVR mEx mRSubst | ||
Definition | df-mvh 31389* | Define the mapping from variables to their variable hypothesis. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mVH mVR mType | ||
Definition | df-mpst 31390* | Define the set of all pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mPreSt mDV mEx mEx | ||
Definition | df-msr 31391* | Define the reduct of a pre-statement. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mStRed mPreSt mVars | ||
Definition | df-msta 31392 | Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mStat mStRed | ||
Definition | df-mfs 31393* | Define the set of all formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mFS mCN mVR mTypemVRmTC mAx mStat mVT mType | ||
Definition | df-mcls 31394* | Define the closure of a set of statements relative to a set of disjointness constraints. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mCls mDV mEx mVH mAx mSubst mVH mVarsmVH mVarsmVH | ||
Definition | df-mpps 31395* | Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mPPSt mPreSt mCls | ||
Definition | df-mthm 31396 | Define the set of theorems. (Contributed by Mario Carneiro, 14-Jul-2016.) |
mThm mStRedmStRedmPPSt | ||
Theorem | mvtval 31397 | The set of variable typecodes. (Contributed by Mario Carneiro, 18-Jul-2016.) |
mVT mType | ||
Theorem | mrexval 31398 | The set of "raw expressions", which are expressions without a typecode, that is, just sequences of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
mCN mVR mREx Word | ||
Theorem | mexval 31399 | The set of expressions, which are pairs whose first element is a typecode, and whose second element is a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.) |
mTC mEx mREx | ||
Theorem | mexval2 31400 | The set of expressions, which are pairs whose first element is a typecode, and whose second element is a list of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016.) |
mTC mEx mCN mVR Word |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |