Home | Metamath
Proof Explorer Theorem List (p. 335 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 | tan2h 33401 | Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.) |
Theorem | pigt3 33402 | is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) |
Theorem | lindsdom 33403 | A linearly independent set in a free linear module of finite dimension over a division ring is smaller than the dimension of the module. (Contributed by Brendan Leahy, 2-Jun-2021.) |
LIndS freeLMod | ||
Theorem | lindsenlbs 33404 | A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021.) |
LIndS freeLMod LBasis freeLMod | ||
Theorem | matunitlindflem1 33405 | One direction of matunitlindf 33407. (Contributed by Brendan Leahy, 2-Jun-2021.) |
Field curry LIndF freeLMod maDet | ||
Theorem | matunitlindflem2 33406 | One direction of matunitlindf 33407. (Contributed by Brendan Leahy, 2-Jun-2021.) |
Field Mat curry LIndF freeLMod maDet Unit | ||
Theorem | matunitlindf 33407 | A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021.) |
Field Mat Unit Mat curry LIndF freeLMod | ||
Theorem | ptrest 33408* | Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019.) |
↾t ↾t | ||
Theorem | ptrecube 33409* | Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.) |
Theorem | poimirlem1 33410* | Lemma for poimir 33442- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.) |
Theorem | poimirlem2 33411* | Lemma for poimir 33442- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.) |
Theorem | poimirlem3 33412* | Lemma for poimir 33442 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ ..^ | ||
Theorem | poimirlem4 33413* | Lemma for poimir 33442 connecting the admissible faces on the back face of the -cube to admissible simplices in the -cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ ..^ | ||
Theorem | poimirlem5 33414* | Lemma for poimir 33442 to establish that, for the simplices defined by a walk along the edges of an -cube, if the starting vertex is not opposite a given face, it is the earliest vertex of the face on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem6 33415* | Lemma for poimir 33442 establishing, for a face of a simplex defined by a walk along the edges of an -cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem7 33416* | Lemma for poimir 33442, similar to poimirlem6 33415, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem8 33417* | Lemma for poimir 33442, establishing that away from the opposite vertex the walks in poimirlem9 33418 yield the same vertices. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem9 33418* | Lemma for poimir 33442, establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem10 33419* | Lemma for poimir 33442 establishing the cube that yields the simplex that yields a face if the opposite vertex was first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem11 33420* | Lemma for poimir 33442 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem12 33421* | Lemma for poimir 33442 connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem13 33422* | Lemma for poimir 33442- for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem14 33423* | Lemma for poimir 33442- for at most one simplex associated with a shared face is the opposite vertex last on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem15 33424* | Lemma for poimir 33442, that the face in poimirlem22 33431 is a face. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem16 33425* | Lemma for poimir 33442 establishing the vertices of the simplex of poimirlem17 33426. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem17 33426* | Lemma for poimir 33442 establishing existence for poimirlem18 33427. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem18 33427* | Lemma for poimir 33442 stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem19 33428* | Lemma for poimir 33442 establishing the vertices of the simplex in poimirlem20 33429. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem20 33429* | Lemma for poimir 33442 establishing existence for poimirlem21 33430. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem21 33430* | Lemma for poimir 33442 stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem22 33431* | Lemma for poimir 33442, that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem23 33432* | Lemma for poimir 33442, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem24 33433* | Lemma for poimir 33442, two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem25 33434* | Lemma for poimir 33442 stating that for a given simplex such that no vertex maps to , the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem26 33435* | Lemma for poimir 33442 showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ ..^ | ||
Theorem | poimirlem27 33436* | Lemma for poimir 33442 showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ ..^ | ||
Theorem | poimirlem28 33437* | Lemma for poimir 33442, a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020.) |
..^ | ||
Theorem | poimirlem29 33438* | Lemma for poimir 33442 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.) |
↾t ..^ ↾t | ||
Theorem | poimirlem30 33439* | Lemma for poimir 33442 combining poimirlem29 33438 with bwth 21213. (Contributed by Brendan Leahy, 21-Aug-2020.) |
↾t ..^ ↾t | ||
Theorem | poimirlem31 33440* | Lemma for poimir 33442, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 33439 and poimirlem28 33437. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
↾t ..^ | ||
Theorem | poimirlem32 33441* | Lemma for poimir 33442, combining poimirlem28 33437, poimirlem30 33439, and poimirlem31 33440 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
↾t ↾t | ||
Theorem | poimir 33442* | Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
↾t | ||
Theorem | broucube 33443* | Brouwer - or as Kulpa calls it, "Bohl-Brouwer" - fixed point theorem for the unit cube. Theorem on [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.) |
↾t ↾t | ||
Theorem | heicant 33444 | Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on [Rosenlicht] p. 80. (Contributed by Brendan Leahy, 13-Aug-2018.) (Proof shortened by AV, 27-Sep-2020.) |
metUnif CnumetUnif | ||
Theorem | opnmbllem0 33445* | Lemma for ismblfin 33450; could also be used to shorten proof of opnmbllem 23369. (Contributed by Brendan Leahy, 13-Jul-2018.) |
Theorem | mblfinlem1 33446* | Lemma for ismblfin 33450, ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in . (Contributed by Brendan Leahy, 13-Jul-2018.) |
Theorem | mblfinlem2 33447* | Lemma for ismblfin 33450, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
Theorem | mblfinlem3 33448* | The difference between two sets measurable by the criterion in ismblfin 33450 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
Theorem | mblfinlem4 33449* | Backward direction of ismblfin 33450. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
Theorem | ismblfin 33450* | Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.) |
Theorem | ovoliunnfl 33451* | ovoliun 23273 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.) |
Theorem | ex-ovoliunnfl 33452* | Demonstration of ovoliunnfl 33451. (Contributed by Brendan Leahy, 21-Nov-2017.) |
Theorem | voliunnfl 33453* | voliun 23322 is incompatible with the Feferman-Levy model; in that model, therefore, the Lebesgue measure as we've defined it isn't actually a measure. (Contributed by Brendan Leahy, 16-Dec-2017.) |
Disj | ||
Theorem | volsupnfl 33454* | volsup 23324 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.) |
Theorem | 0mbf 33455 | The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.) |
MblFn | ||
Theorem | mbfresfi 33456* | Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.) |
MblFn MblFn | ||
Theorem | mbfposadd 33457* | If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018.) |
MblFn MblFn MblFn MblFn | ||
Theorem | cnambfre 33458 | A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.) |
↾t MblFn | ||
Theorem | dvtanlem 33459 | Lemma for dvtan 33460- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) (Proof shortened by OpenAI, 3-Jul-2020.) |
ℂfld | ||
Theorem | dvtan 33460 | Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.) |
Theorem | itg2addnclem 33461* | An alternate expression for the integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017.) (Revised by Brendan Leahy, 10-Mar-2018.) |
Theorem | itg2addnclem2 33462* | Lemma for itg2addnc 33464. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.) |
MblFn | ||
Theorem | itg2addnclem3 33463* | Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 33464. (Contributed by Brendan Leahy, 11-Mar-2018.) |
MblFn | ||
Theorem | itg2addnc 33464 | Alternate proof of itg2add 23526 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 23475, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 9257, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) (Revised by Brendan Leahy, 13-Mar-2018.) |
MblFn | ||
Theorem | itg2gt0cn 33465* | itg2gt0 23527 holds on functions continuous on an open interval in the absence of ax-cc 9257. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.) |
Theorem | ibladdnclem 33466* | Lemma for ibladdnc 33467; cf ibladdlem 23586, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 33464. (Contributed by Brendan Leahy, 31-Oct-2017.) |
MblFn | ||
Theorem | ibladdnc 33467* | Choice-free analogue of itgadd 23591. A measurability hypothesis is necessitated by the loss of mbfadd 23428; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017.) |
MblFn | ||
Theorem | itgaddnclem1 33468* | Lemma for itgaddnc 33470; cf. itgaddlem1 23589. (Contributed by Brendan Leahy, 7-Nov-2017.) |
MblFn | ||
Theorem | itgaddnclem2 33469* | Lemma for itgaddnc 33470; cf. itgaddlem2 23590. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.) |
MblFn | ||
Theorem | itgaddnc 33470* | Choice-free analogue of itgadd 23591. (Contributed by Brendan Leahy, 11-Nov-2017.) |
MblFn | ||
Theorem | iblsubnc 33471* | Choice-free analogue of iblsub 23588. (Contributed by Brendan Leahy, 11-Nov-2017.) |
MblFn | ||
Theorem | itgsubnc 33472* | Choice-free analogue of itgsub 23592. (Contributed by Brendan Leahy, 11-Nov-2017.) |
MblFn | ||
Theorem | iblabsnclem 33473* | Lemma for iblabsnc 33474; cf. iblabslem 23594. (Contributed by Brendan Leahy, 7-Nov-2017.) |
MblFn | ||
Theorem | iblabsnc 33474* | Choice-free analogue of iblabs 23595. As with ibladdnc 33467, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.) |
MblFn | ||
Theorem | iblmulc2nc 33475* | Choice-free analogue of iblmulc2 23597. (Contributed by Brendan Leahy, 17-Nov-2017.) |
MblFn | ||
Theorem | itgmulc2nclem1 33476* | Lemma for itgmulc2nc 33478; cf. itgmulc2lem1 23598. (Contributed by Brendan Leahy, 17-Nov-2017.) |
MblFn | ||
Theorem | itgmulc2nclem2 33477* | Lemma for itgmulc2nc 33478; cf. itgmulc2lem2 23599. (Contributed by Brendan Leahy, 19-Nov-2017.) |
MblFn | ||
Theorem | itgmulc2nc 33478* | Choice-free analogue of itgmulc2 23600. (Contributed by Brendan Leahy, 19-Nov-2017.) |
MblFn | ||
Theorem | itgabsnc 33479* | Choice-free analogue of itgabs 23601. (Contributed by Brendan Leahy, 19-Nov-2017.) (Revised by Brendan Leahy, 19-Jun-2018.) |
MblFn MblFn | ||
Theorem | bddiblnc 33480* | Choice-free proof of bddibl 23606. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.) |
MblFn | ||
Theorem | cnicciblnc 33481 | Choice-free proof of cniccibl 23607. (Contributed by Brendan Leahy, 2-Nov-2017.) |
Theorem | itggt0cn 33482* | itggt0 23608 holds for continuous functions in the absence of ax-cc 9257. (Contributed by Brendan Leahy, 16-Nov-2017.) |
Theorem | ftc1cnnclem 33483* | Lemma for ftc1cnnc 33484; cf. ftc1lem4 23802. The stronger assumptions of ftc1cn 23806 are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017.) |
Theorem | ftc1cnnc 33484* | Choice-free proof of ftc1cn 23806. (Contributed by Brendan Leahy, 20-Nov-2017.) |
Theorem | ftc1anclem1 33485 | Lemma for ftc1anc 33493- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 23425, but this proof avoids ax-cc 9257. (Contributed by Brendan Leahy, 18-Jun-2018.) |
MblFn MblFn | ||
Theorem | ftc1anclem2 33486* | Lemma for ftc1anc 33493- restriction of an integrable function to the absolute value of its real or imaginary part. (Contributed by Brendan Leahy, 19-Jun-2018.) (Revised by Brendan Leahy, 8-Aug-2018.) |
Theorem | ftc1anclem3 33487 | Lemma for ftc1anc 33493- the absolute value of the sum of a simple function and times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.) |
Theorem | ftc1anclem4 33488* | Lemma for ftc1anc 33493. (Contributed by Brendan Leahy, 17-Jun-2018.) |
Theorem | ftc1anclem5 33489* | Lemma for ftc1anc 33493, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.) |
Theorem | ftc1anclem6 33490* | Lemma for ftc1anc 33493- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued . (Contributed by Brendan Leahy, 31-May-2018.) |
Theorem | ftc1anclem7 33491* | Lemma for ftc1anc 33493. (Contributed by Brendan Leahy, 13-May-2018.) |
Theorem | ftc1anclem8 33492* | Lemma for ftc1anc 33493. (Contributed by Brendan Leahy, 29-May-2018.) |
Theorem | ftc1anc 33493* | ftc1a 23800 holds for functions that obey the triangle inequality in the absence of ax-cc 9257. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.) |
Theorem | ftc2nc 33494* | Choice-free proof of ftc2 23807. (Contributed by Brendan Leahy, 19-Jun-2018.) |
Theorem | asindmre 33495 | Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018.) |
Theorem | dvasin 33496* | Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
arcsin | ||
Theorem | dvacos 33497* | Derivative of arccosine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
arccos | ||
Theorem | dvreasin 33498 | Real derivative of arcsine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.) |
arcsin | ||
Theorem | dvreacos 33499 | Real derivative of arccosine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.) |
arccos | ||
Theorem | areacirclem1 33500* | Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
arcsin |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |