Home | Metamath
Proof Explorer Theorem List (p. 233 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 | minveclem4a 23201* | Lemma for minvec 23207. converges to a point in . (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
↾s CMetSp inf | ||
Theorem | minveclem4b 23202* | Lemma for minvec 23207. The convergent point of the Cauchy sequence is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
↾s CMetSp inf | ||
Theorem | minveclem4 23203* | Lemma for minvec 23207. The convergent point of the Cauchy sequence attains the minimum distance, and so is closer to than any other point in . (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.) |
↾s CMetSp inf | ||
Theorem | minveclem5 23204* | Lemma for minvec 23207. Discharge the assumptions in minveclem4 23203. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
↾s CMetSp inf | ||
Theorem | minveclem6 23205* | Lemma for minvec 23207. Any minimal point is less than away from . (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.) |
↾s CMetSp inf | ||
Theorem | minveclem7 23206* | Lemma for minvec 23207. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
↾s CMetSp inf | ||
Theorem | minvec 23207* | Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace that minimizes the distance to an arbitrary vector in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 3-Oct-2020.) |
↾s CMetSp | ||
Theorem | pjthlem1 23208* | Lemma for pjth 23210. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 17-Oct-2015.) |
Theorem | pjthlem2 23209 | Lemma for pjth 23210. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) |
Theorem | pjth 23210 | Projection Theorem: Any Hilbert space vector can be decomposed uniquely into a member of a closed subspace and a member of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.) |
Theorem | pjth2 23211 | Projection Theorem with abbreviations: A topologically closed subspace is a projection subspace. (Contributed by Mario Carneiro, 17-Oct-2015.) |
Theorem | cldcss 23212 | Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.) |
Theorem | cldcss2 23213 | Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.) |
Theorem | hlhil 23214 | Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015.) |
Theorem | mulcncf 23215* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | divcncf 23216* | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | pmltpclem1 23217* | Lemma for pmltpc 23219. (Contributed by Mario Carneiro, 1-Jul-2014.) |
Theorem | pmltpclem2 23218* | Lemma for pmltpc 23219. (Contributed by Mario Carneiro, 1-Jul-2014.) |
Theorem | pmltpc 23219* | Any function on the reals is either increasing, decreasing, or has a triple of points in a vee formation. (This theorem was created on demand by Mario Carneiro for the 6PCM conference in Bialystok, 1-Jul-2014.) (Contributed by Mario Carneiro, 1-Jul-2014.) |
Theorem | ivthlem1 23220* | Lemma for ivth 23223. The set of all values with less than is lower bounded by and upper bounded by . (Contributed by Mario Carneiro, 17-Jun-2014.) |
Theorem | ivthlem2 23221* | Lemma for ivth 23223. Show that the supremum of cannot be less than . If it was, continuity of implies that there are points just above the supremum that are also less than , a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014.) |
Theorem | ivthlem3 23222* | Lemma for ivth 23223, the intermediate value theorem. Show that cannot be greater than , and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 17-Jun-2014.) |
Theorem | ivth 23223* | The intermediate value theorem, increasing case. This is Metamath 100 proof #79. (Contributed by Paul Chapman, 22-Jan-2008.) (Proof shortened by Mario Carneiro, 30-Apr-2014.) |
Theorem | ivth2 23224* | The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Theorem | ivthle 23225* | The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014.) |
Theorem | ivthle2 23226* | The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014.) |
Theorem | ivthicc 23227* | The interval between any two points of a continuous real function is contained in the range of the function. Equivalently, the range of a continuous real function is convex. (Contributed by Mario Carneiro, 12-Aug-2014.) |
Theorem | evthicc 23228* | Specialization of the Extreme Value Theorem to a closed interval of . (Contributed by Mario Carneiro, 12-Aug-2014.) |
Theorem | evthicc2 23229* | Combine ivthicc 23227 with evthicc 23228 to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015.) |
Theorem | cniccbdd 23230* | A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014.) |
Syntax | covol 23231 | Extend class notation with the outer Lebesgue measure. |
Syntax | cvol 23232 | Extend class notation with the Lebesgue measure. |
Definition | df-ovol 23233* | Define the outer Lebesgue measure for subsets of the reals. Here is a function from the positive integers to pairs with , and the outer volume of the set is the infimum over all such functions such that the union of the open intervals covers of the sum of . (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.) |
inf | ||
Definition | df-vol 23234* | Define the Lebesgue measure, which is just the outer measure with a peculiar domain of definition. The property of being Lebesgue-measurable can be expressed as . (Contributed by Mario Carneiro, 17-Mar-2014.) |
Theorem | ovolfcl 23235 | Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolfioo 23236* | Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolficc 23237* | Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolficcss 23238 | Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015.) |
Theorem | ovolfsval 23239 | The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolfsf 23240 | Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolsf 23241 | Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolval 23242* | The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.) |
inf | ||
Theorem | elovolm 23243* | Elementhood in the set of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | elovolmr 23244* | Sufficient condition for elementhood in the set . (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolmge0 23245* | The set is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolcl 23246 | The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovollb 23247 | The outer volume is a lower bound on the sum of all interval coverings of . (Contributed by Mario Carneiro, 15-Jun-2014.) |
Theorem | ovolgelb 23248* | The outer volume is the greatest lower bound on the sum of all interval coverings of . (Contributed by Mario Carneiro, 15-Jun-2014.) |
Theorem | ovolge0 23249 | The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolf 23250 | The domain and range of the outer volume function. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
Theorem | ovollecl 23251 | If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.) |
Theorem | ovolsslem 23252* | Lemma for ovolss 23253. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
Theorem | ovolss 23253 | The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.) |
Theorem | ovolsscl 23254 | If a set is contained in another of bounded measure, it too is bounded. (Contributed by Mario Carneiro, 18-Mar-2014.) |
Theorem | ovolssnul 23255 | A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014.) |
Theorem | ovollb2lem 23256* | Lemma for ovollb2 23257. (Contributed by Mario Carneiro, 24-Mar-2015.) |
Theorem | ovollb2 23257 | It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb 23247). (Contributed by Mario Carneiro, 24-Mar-2015.) |
Theorem | ovolctb 23258 | The volume of a denumerable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.) |
Theorem | ovolq 23259 | The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
Theorem | ovolctb2 23260 | The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) |
Theorem | ovol0 23261 | The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
Theorem | ovolfi 23262 | A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014.) |
Theorem | ovolsn 23263 | A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014.) |
Theorem | ovolunlem1a 23264* | Lemma for ovolun 23267. (Contributed by Mario Carneiro, 7-May-2015.) |
Theorem | ovolunlem1 23265* | Lemma for ovolun 23267. (Contributed by Mario Carneiro, 12-Jun-2014.) |
Theorem | ovolunlem2 23266 | Lemma for ovolun 23267. (Contributed by Mario Carneiro, 12-Jun-2014.) |
Theorem | ovolun 23267 | The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 23273, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
Theorem | ovolunnul 23268 | Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.) |
Theorem | ovolfiniun 23269* | The Lebesgue outer measure function is finitely sub-additive. Finite sum version. (Contributed by Mario Carneiro, 19-Jun-2014.) |
Theorem | ovoliunlem1 23270* | Lemma for ovoliun 23273. (Contributed by Mario Carneiro, 12-Jun-2014.) |
Theorem | ovoliunlem2 23271* | Lemma for ovoliun 23273. (Contributed by Mario Carneiro, 12-Jun-2014.) |
Theorem | ovoliunlem3 23272* | Lemma for ovoliun 23273. (Contributed by Mario Carneiro, 12-Jun-2014.) |
Theorem | ovoliun 23273* | The Lebesgue outer measure function is countably sub-additive. (Many books allow as a value for one of the sets in the sum, but in our setup we can't do arithmetic on infinity, and in any case the volume of a union containing an infinitely large set is already infinitely large by monotonicity ovolss 23253, so we need not consider this case here, although we do allow the sum itself to be infinite.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
Theorem | ovoliun2 23274* | The Lebesgue outer measure function is countably sub-additive. (This version is a little easier to read, but does not allow infinite values like ovoliun 23273.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
Theorem | ovoliunnul 23275* | A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015.) |
Theorem | shft2rab 23276* | If is a shift of by , then is a shift of by . (Contributed by Mario Carneiro, 22-Mar-2014.) (Revised by Mario Carneiro, 6-Apr-2015.) |
Theorem | ovolshftlem1 23277* | Lemma for ovolshft 23279. (Contributed by Mario Carneiro, 22-Mar-2014.) |
Theorem | ovolshftlem2 23278* | Lemma for ovolshft 23279. (Contributed by Mario Carneiro, 22-Mar-2014.) |
Theorem | ovolshft 23279* | The Lebesgue outer measure function is shift-invariant. (Contributed by Mario Carneiro, 22-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
Theorem | sca2rab 23280* | If is a scale of by , then is a scale of by . (Contributed by Mario Carneiro, 22-Mar-2014.) |
Theorem | ovolscalem1 23281* | Lemma for ovolsca 23283. (Contributed by Mario Carneiro, 6-Apr-2015.) |
Theorem | ovolscalem2 23282* | Lemma for ovolshft 23279. (Contributed by Mario Carneiro, 22-Mar-2014.) |
Theorem | ovolsca 23283* | The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.) |
Theorem | ovolicc1 23284* | The measure of a closed interval is lower bounded by its length. (Contributed by Mario Carneiro, 13-Jun-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.) |
Theorem | ovolicc2lem1 23285* | Lemma for ovolicc2 23290. (Contributed by Mario Carneiro, 14-Jun-2014.) |
Theorem | ovolicc2lem2 23286* | Lemma for ovolicc2 23290. (Contributed by Mario Carneiro, 14-Jun-2014.) |
Theorem | ovolicc2lem3 23287* | Lemma for ovolicc2 23290. (Contributed by Mario Carneiro, 14-Jun-2014.) |
Theorem | ovolicc2lem4 23288* | Lemma for ovolicc2 23290. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by AV, 17-Sep-2020.) |
inf | ||
Theorem | ovolicc2lem5 23289* | Lemma for ovolicc2 23290. (Contributed by Mario Carneiro, 14-Jun-2014.) |
Theorem | ovolicc2 23290* | The measure of a closed interval is upper bounded by its length. (Contributed by Mario Carneiro, 14-Jun-2014.) |
Theorem | ovolicc 23291 | The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
Theorem | ovolicopnf 23292 | The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
Theorem | ovolre 23293 | The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.) |
Theorem | ismbl 23294* | The predicate " is Lebesgue-measurable". A set is measurable if it splits every other set in a "nice" way, that is, if the measure of the pieces and sum up to the measure of (assuming that the measure of is a real number, so that this addition makes sense). (Contributed by Mario Carneiro, 17-Mar-2014.) |
Theorem | ismbl2 23295* | From ovolun 23267, it suffices to show that the measure of is at least the sum of the measures of and . (Contributed by Mario Carneiro, 15-Jun-2014.) |
Theorem | volres 23296 | A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014.) |
Theorem | volf 23297 | The domain and range of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014.) |
Theorem | mblvol 23298 | The volume of a measurable set is the same as its outer volume. (Contributed by Mario Carneiro, 17-Mar-2014.) |
Theorem | mblss 23299 | A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014.) |
Theorem | mblsplit 23300 | The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |