![]() |
Metamath
Proof Explorer Theorem List (p. 372 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ftc1anclem1 37101 | Lemma for ftc1anc 37109- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 25574, but this proof avoids ax-cc 10450. (Contributed by Brendan Leahy, 18-Jun-2018.) |
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β (abs β πΉ) β MblFn) | ||
Theorem | ftc1anclem2 37102* | Lemma for ftc1anc 37109- 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.) |
β’ ((πΉ:π΄βΆβ β§ πΉ β πΏ1 β§ πΊ β {β, β}) β (β«2β(π‘ β β β¦ if(π‘ β π΄, (absβ(πΊβ(πΉβπ‘))), 0))) β β) | ||
Theorem | ftc1anclem3 37103 | Lemma for ftc1anc 37109- the absolute value of the sum of a simple function and i times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.) |
β’ ((πΉ β dom β«1 β§ πΊ β dom β«1) β (abs β (πΉ βf + ((β Γ {i}) βf Β· πΊ))) β dom β«1) | ||
Theorem | ftc1anclem4 37104* | Lemma for ftc1anc 37109. (Contributed by Brendan Leahy, 17-Jun-2018.) |
β’ ((πΉ β dom β«1 β§ πΊ β πΏ1 β§ πΊ:ββΆβ) β (β«2β(π‘ β β β¦ (absβ((πΊβπ‘) β (πΉβπ‘))))) β β) | ||
Theorem | ftc1anclem5 37105* | Lemma for ftc1anc 37109, 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.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) β β’ ((π β§ π β β+) β βπ β dom β«1(β«2β(π‘ β β β¦ (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π) | ||
Theorem | ftc1anclem6 37106* | Lemma for ftc1anc 37109- 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.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) β β’ ((π β§ π β β+) β βπ β dom β«1βπ β dom β«1(β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < π) | ||
Theorem | ftc1anclem7 37107* | Lemma for ftc1anc 37109. (Contributed by Brendan Leahy, 13-May-2018.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) β β’ (((((((π β§ (π β dom β«1 β§ π β dom β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran π βͺ ran π)), β, < )))) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) < ((π¦ / 2) + (π¦ / 2))) | ||
Theorem | ftc1anclem8 37108* | Lemma for ftc1anc 37109. (Contributed by Brendan Leahy, 29-May-2018.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) β β’ (((((((π β§ (π β dom β«1 β§ π β dom β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran π βͺ ran π)), β, < )))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) < π¦) | ||
Theorem | ftc1anc 37109* | ftc1a 25959 holds for functions that obey the triangle inequality in the absence of ax-cc 10450. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) & β’ (π β βπ β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))(absββ«π (πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ(πΉβπ‘)), 0)))) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | ftc2nc 37110* | Choice-free proof of ftc2 25966. (Contributed by Brendan Leahy, 19-Jun-2018.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (β D πΉ) β ((π΄(,)π΅)βcnββ)) & β’ (π β (β D πΉ) β πΏ1) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | asindmre 37111 | Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (π· β© β) = (-1(,)1) | ||
Theorem | dvasin 37112* | Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (β D (arcsin βΎ π·)) = (π₯ β π· β¦ (1 / (ββ(1 β (π₯β2))))) | ||
Theorem | dvacos 37113* | Derivative of arccosine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (β D (arccos βΎ π·)) = (π₯ β π· β¦ (-1 / (ββ(1 β (π₯β2))))) | ||
Theorem | dvreasin 37114 | Real derivative of arcsine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.) |
β’ (β D (arcsin βΎ (-1(,)1))) = (π₯ β (-1(,)1) β¦ (1 / (ββ(1 β (π₯β2))))) | ||
Theorem | dvreacos 37115 | Real derivative of arccosine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.) |
β’ (β D (arccos βΎ (-1(,)1))) = (π₯ β (-1(,)1) β¦ (-1 / (ββ(1 β (π₯β2))))) | ||
Theorem | areacirclem1 37116* | Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
β’ (π β β+ β (β D (π‘ β (-π (,)π ) β¦ ((π β2) Β· ((arcsinβ(π‘ / π )) + ((π‘ / π ) Β· (ββ(1 β ((π‘ / π )β2)))))))) = (π‘ β (-π (,)π ) β¦ (2 Β· (ββ((π β2) β (π‘β2)))))) | ||
Theorem | areacirclem2 37117* | Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
β’ ((π β β β§ 0 β€ π ) β (π‘ β (-π [,]π ) β¦ (ββ((π β2) β (π‘β2)))) β ((-π [,]π )βcnββ)) | ||
Theorem | areacirclem3 37118* | Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
β’ ((π β β β§ 0 β€ π ) β (π‘ β (-π [,]π ) β¦ (2 Β· (ββ((π β2) β (π‘β2))))) β πΏ1) | ||
Theorem | areacirclem4 37119* | Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
β’ (π β β+ β (π‘ β (-π [,]π ) β¦ ((π β2) Β· ((arcsinβ(π‘ / π )) + ((π‘ / π ) Β· (ββ(1 β ((π‘ / π )β2))))))) β ((-π [,]π )βcnββ)) | ||
Theorem | areacirclem5 37120* | Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β β β§ π¦ β β) β§ ((π₯β2) + (π¦β2)) β€ (π β2))} β β’ ((π β β β§ 0 β€ π β§ π‘ β β) β (π β {π‘}) = if((absβπ‘) β€ π , (-(ββ((π β2) β (π‘β2)))[,](ββ((π β2) β (π‘β2)))), β )) | ||
Theorem | areacirc 37121* | The area of a circle of radius π is Ο Β· π β2. This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β β β§ π¦ β β) β§ ((π₯β2) + (π¦β2)) β€ (π β2))} β β’ ((π β β β§ 0 β€ π ) β (areaβπ) = (Ο Β· (π β2))) | ||
Theorem | unirep 37122* | Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011.) |
β’ (π¦ = π· β (π β π)) & β’ (π¦ = π· β π΅ = πΆ) & β’ (π¦ = π§ β (π β π)) & β’ (π¦ = π§ β π΅ = πΉ) & β’ π΅ β V β β’ ((βπ¦ β π΄ βπ§ β π΄ ((π β§ π) β π΅ = πΉ) β§ (π· β π΄ β§ π)) β (β©π₯βπ¦ β π΄ (π β§ π₯ = π΅)) = πΆ) | ||
Theorem | cover2 37123* | Two ways of expressing the statement "there is a cover of π΄ by elements of π΅ such that for each set in the cover, π". Note that π and π₯ must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010.) |
β’ π΅ β V & β’ π΄ = βͺ π΅ β β’ (βπ₯ β π΄ βπ¦ β π΅ (π₯ β π¦ β§ π) β βπ§ β π« π΅(βͺ π§ = π΄ β§ βπ¦ β π§ π)) | ||
Theorem | cover2g 37124* | Two ways of expressing the statement "there is a cover of π΄ by elements of π΅ such that for each set in the cover, π". Note that π and π₯ must be distinct. (Contributed by Jeff Madsen, 21-Jun-2010.) |
β’ π΄ = βͺ π΅ β β’ (π΅ β πΆ β (βπ₯ β π΄ βπ¦ β π΅ (π₯ β π¦ β§ π) β βπ§ β π« π΅(βͺ π§ = π΄ β§ βπ¦ β π§ π))) | ||
Theorem | brabg2 37125* | Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ π = {β¨π₯, π¦β© β£ π} & β’ (π β π΄ β πΆ) β β’ (π΅ β π· β (π΄π π΅ β π)) | ||
Theorem | opelopab3 37126* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ (π β π΄ β πΆ) β β’ (π΅ β π· β (β¨π΄, π΅β© β {β¨π₯, π¦β© β£ π} β π)) | ||
Theorem | cocanfo 37127 | Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
β’ (((πΉ:π΄βontoβπ΅ β§ πΊ Fn π΅ β§ π» Fn π΅) β§ (πΊ β πΉ) = (π» β πΉ)) β πΊ = π») | ||
Theorem | brresi2 37128 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π΅ β V β β’ (π΄(π βΎ πΆ)π΅ β π΄π π΅) | ||
Theorem | fnopabeqd 37129* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |
β’ (π β π΅ = πΆ) β β’ (π β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = π΅)} = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = πΆ)}) | ||
Theorem | fvopabf4g 37130* | Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
β’ πΆ β V & β’ (π₯ = π΄ β π΅ = πΆ) & β’ πΉ = (π₯ β (π βm π·) β¦ π΅) β β’ ((π· β π β§ π β π β§ π΄:π·βΆπ ) β (πΉβπ΄) = πΆ) | ||
Theorem | fnopabco 37131* | Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ (π₯ β π΄ β π΅ β πΆ) & β’ πΉ = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = π΅)} & β’ πΊ = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = (π»βπ΅))} β β’ (π» Fn πΆ β πΊ = (π» β πΉ)) | ||
Theorem | opropabco 37132* | Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
β’ (π₯ β π΄ β π΅ β π ) & β’ (π₯ β π΄ β πΆ β π) & β’ πΉ = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = β¨π΅, πΆβ©)} & β’ πΊ = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = (π΅ππΆ))} β β’ (π Fn (π Γ π) β πΊ = (π β πΉ)) | ||
Theorem | cocnv 37133 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((Fun πΉ β§ Fun πΊ) β ((πΉ β πΊ) β β‘πΊ) = (πΉ βΎ ran πΊ)) | ||
Theorem | f1ocan1fv 37134 | Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
β’ ((Fun πΉ β§ πΊ:π΄β1-1-ontoβπ΅ β§ π β π΅) β ((πΉ β πΊ)β(β‘πΊβπ)) = (πΉβπ)) | ||
Theorem | f1ocan2fv 37135 | Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((Fun πΉ β§ πΊ:π΄β1-1-ontoβπ΅ β§ π β π΄) β ((πΉ β β‘πΊ)β(πΊβπ)) = (πΉβπ)) | ||
Theorem | inixp 37136* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (Xπ₯ β π΄ π΅ β© Xπ₯ β π΄ πΆ) = Xπ₯ β π΄ (π΅ β© πΆ) | ||
Theorem | upixp 37137* | Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ π = Xπ β π΄ (πΆβπ) & β’ π = (π€ β π΄ β¦ (π₯ β π β¦ (π₯βπ€))) β β’ ((π΄ β π β§ π΅ β π β§ βπ β π΄ (πΉβπ):π΅βΆ(πΆβπ)) β β!β(β:π΅βΆπ β§ βπ β π΄ (πΉβπ) = ((πβπ) β β))) | ||
Theorem | abrexdom 37138* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π¦ β π΄ β β*π₯π) β β’ (π΄ β π β {π₯ β£ βπ¦ β π΄ π} βΌ π΄) | ||
Theorem | abrexdom2 37139* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β π β {π₯ β£ βπ¦ β π΄ π₯ = π΅} βΌ π΄) | ||
Theorem | ac6gf 37140* | Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ β²π¦π & β’ (π¦ = (πβπ₯) β (π β π)) β β’ ((π΄ β πΆ β§ βπ₯ β π΄ βπ¦ β π΅ π) β βπ(π:π΄βΆπ΅ β§ βπ₯ β π΄ π)) | ||
Theorem | indexa 37141* | If for every element of an indexing set π΄ there exists a corresponding element of another set π΅, then there exists a subset of π΅ consisting only of those elements which are indexed by π΄. Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π΅ β π β§ βπ₯ β π΄ βπ¦ β π΅ π) β βπ(π β π΅ β§ βπ₯ β π΄ βπ¦ β π π β§ βπ¦ β π βπ₯ β π΄ π)) | ||
Theorem | indexdom 37142* | If for every element of an indexing set π΄ there exists a corresponding element of another set π΅, then there exists a subset of π΅ consisting only of those elements which are indexed by π΄, and which is dominated by the set π΄. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π΄ β π β§ βπ₯ β π΄ βπ¦ β π΅ π) β βπ((π βΌ π΄ β§ π β π΅) β§ (βπ₯ β π΄ βπ¦ β π π β§ βπ¦ β π βπ₯ β π΄ π))) | ||
Theorem | frinfm 37143* | A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π Fr π΄ β§ (π΅ β πΆ β§ π΅ β π΄ β§ π΅ β β )) β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΄ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§))) | ||
Theorem | welb 37144* | A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π We π΄ β§ (π΅ β πΆ β§ π΅ β π΄ β§ π΅ β β )) β (β‘π Or π΅ β§ βπ₯ β π΅ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΅ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§)))) | ||
Theorem | supex2g 37145 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β πΆ β sup(π΅, π΄, π ) β V) | ||
Theorem | supclt 37146* | Closure of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π Or π΄ β§ βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β sup(π΅, π΄, π ) β π΄) | ||
Theorem | supubt 37147* | Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π Or π΄ β§ βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β (πΆ β π΅ β Β¬ sup(π΅, π΄, π )π πΆ)) | ||
Theorem | filbcmb 37148* | Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π΄ β Fin β§ π΄ β β β§ π΅ β β) β (βπ₯ β π΄ βπ¦ β π΅ βπ§ β π΅ (π¦ β€ π§ β π) β βπ¦ β π΅ βπ§ β π΅ (π¦ β€ π§ β βπ₯ β π΄ π))) | ||
Theorem | fzmul 37149 | Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β) β (π½ β (π...π) β (πΎ Β· π½) β ((πΎ Β· π)...(πΎ Β· π)))) | ||
Theorem | sdclem2 37150* | Lemma for sdc 37152. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = (β€β₯βπ) & β’ (π = (π βΎ (π...π)) β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π = β β§ π = (π + 1)) β (π β π)) & β’ (π β π΄ β π) & β’ (π β π β β€) & β’ (π β βπ(π:{π}βΆπ΄ β§ π)) & β’ ((π β§ π β π) β ((π:(π...π)βΆπ΄ β§ π) β ββ(β:(π...(π + 1))βΆπ΄ β§ π = (β βΎ (π...π)) β§ π))) & β’ π½ = {π β£ βπ β π (π:(π...π)βΆπ΄ β§ π)} & β’ πΉ = (π€ β π, π₯ β π½ β¦ {β β£ βπ β π (β:(π...(π + 1))βΆπ΄ β§ π₯ = (β βΎ (π...π)) β§ π)}) & β’ β²ππ & β’ (π β πΊ:πβΆπ½) & β’ (π β (πΊβπ):(π...π)βΆπ΄) & β’ ((π β§ π€ β π) β (πΊβ(π€ + 1)) β (π€πΉ(πΊβπ€))) β β’ (π β βπ(π:πβΆπ΄ β§ βπ β π π)) | ||
Theorem | sdclem1 37151* | Lemma for sdc 37152. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = (β€β₯βπ) & β’ (π = (π βΎ (π...π)) β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π = β β§ π = (π + 1)) β (π β π)) & β’ (π β π΄ β π) & β’ (π β π β β€) & β’ (π β βπ(π:{π}βΆπ΄ β§ π)) & β’ ((π β§ π β π) β ((π:(π...π)βΆπ΄ β§ π) β ββ(β:(π...(π + 1))βΆπ΄ β§ π = (β βΎ (π...π)) β§ π))) & β’ π½ = {π β£ βπ β π (π:(π...π)βΆπ΄ β§ π)} & β’ πΉ = (π€ β π, π₯ β π½ β¦ {β β£ βπ β π (β:(π...(π + 1))βΆπ΄ β§ π₯ = (β βΎ (π...π)) β§ π)}) β β’ (π β βπ(π:πβΆπ΄ β§ βπ β π π)) | ||
Theorem | sdc 37152* | Strong dependent choice. Suppose we may choose an element of π΄ such that property π holds, and suppose that if we have already chosen the first π elements (represented here by a function from 1...π to π΄), we may choose another element so that all π + 1 elements taken together have property π. Then there exists an infinite sequence of elements of π΄ such that the first π terms of this sequence satisfy π for all π. This theorem allows to construct infinite sequences where each term depends on all the previous terms in the sequence. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 3-Jun-2014.) |
β’ π = (β€β₯βπ) & β’ (π = (π βΎ (π...π)) β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π = β β§ π = (π + 1)) β (π β π)) & β’ (π β π΄ β π) & β’ (π β π β β€) & β’ (π β βπ(π:{π}βΆπ΄ β§ π)) & β’ ((π β§ π β π) β ((π:(π...π)βΆπ΄ β§ π) β ββ(β:(π...(π + 1))βΆπ΄ β§ π = (β βΎ (π...π)) β§ π))) β β’ (π β βπ(π:πβΆπ΄ β§ βπ β π π)) | ||
Theorem | fdc 37153* | Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010.) |
β’ π΄ β V & β’ π β β€ & β’ π = (β€β₯βπ) & β’ π = (π + 1) & β’ (π = (πβ(π β 1)) β (π β π)) & β’ (π = (πβπ) β (π β π)) & β’ (π = (πβπ) β (π β π)) & β’ (π β πΆ β π΄) & β’ (π β π Fr π΄) & β’ ((π β§ π β π΄) β (π β¨ βπ β π΄ π)) & β’ (((π β§ π) β§ (π β π΄ β§ π β π΄)) β ππ π) β β’ (π β βπ β π βπ(π:(π...π)βΆπ΄ β§ ((πβπ) = πΆ β§ π) β§ βπ β (π...π)π)) | ||
Theorem | fdc1 37154* | Variant of fdc 37153 with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010.) |
β’ π΄ β V & β’ π β β€ & β’ π = (β€β₯βπ) & β’ π = (π + 1) & β’ (π = (πβπ) β (π β π)) & β’ (π = (πβ(π β 1)) β (π β π)) & β’ (π = (πβπ) β (π β π)) & β’ (π = (πβπ) β (π β π)) & β’ (π β βπ β π΄ π) & β’ (π β π Fr π΄) & β’ ((π β§ π β π΄) β (π β¨ βπ β π΄ π)) & β’ (((π β§ π) β§ (π β π΄ β§ π β π΄)) β ππ π) β β’ (π β βπ β π βπ(π:(π...π)βΆπ΄ β§ (π β§ π) β§ βπ β (π...π)π)) | ||
Theorem | seqpo 37155* | Two ways to say that a sequence respects a partial order. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π Po π΄ β§ πΉ:ββΆπ΄) β (βπ β β (πΉβπ )π (πΉβ(π + 1)) β βπ β β βπ β (β€β₯β(π + 1))(πΉβπ)π (πΉβπ))) | ||
Theorem | incsequz 37156* | An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1)) β§ π΄ β β) β βπ β β (πΉβπ) β (β€β₯βπ΄)) | ||
Theorem | incsequz2 37157* | An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1)) β§ π΄ β β) β βπ β β βπ β (β€β₯βπ)(πΉβπ) β (β€β₯βπ΄)) | ||
Theorem | nnubfi 37158* | A bounded above set of positive integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.) |
β’ ((π΄ β β β§ π΅ β β) β {π₯ β π΄ β£ π₯ < π΅} β Fin) | ||
Theorem | nninfnub 37159* | An infinite set of positive integers is unbounded above. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.) |
β’ ((π΄ β β β§ Β¬ π΄ β Fin β§ π΅ β β) β {π₯ β π΄ β£ π΅ < π₯} β β ) | ||
Theorem | subspopn 37160 | An open set is open in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
β’ (((π½ β Top β§ π΄ β π) β§ (π΅ β π½ β§ π΅ β π΄)) β π΅ β (π½ βΎt π΄)) | ||
Theorem | neificl 37161 | Neighborhoods are closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Nov-2013.) |
β’ (((π½ β Top β§ π β ((neiβπ½)βπ)) β§ (π β Fin β§ π β β )) β β© π β ((neiβπ½)βπ)) | ||
Theorem | lpss2 37162 | Limit points of a subset are limit points of the larger set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ π΅ β π΄) β ((limPtβπ½)βπ΅) β ((limPtβπ½)βπ΄)) | ||
Theorem | metf1o 37163* | Use a bijection with a metric space to construct a metric on a set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = (π₯ β π, π¦ β π β¦ ((πΉβπ₯)π(πΉβπ¦))) β β’ ((π β π΄ β§ π β (Metβπ) β§ πΉ:πβ1-1-ontoβπ) β π β (Metβπ)) | ||
Theorem | blssp 37164 | A ball in the subspace metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jan-2014.) |
β’ π = (π βΎ (π Γ π)) β β’ (((π β (Metβπ) β§ π β π) β§ (π β π β§ π β β+)) β (π(ballβπ)π ) = ((π(ballβπ)π ) β© π)) | ||
Theorem | mettrifi 37165* | Generalized triangle inequality for arbitrary finite sums. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.) |
β’ (π β π· β (Metβπ)) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β π) β β’ (π β ((πΉβπ)π·(πΉβπ)) β€ Ξ£π β (π...(π β 1))((πΉβπ)π·(πΉβ(π + 1)))) | ||
Theorem | lmclim2 37166* | A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
β’ (π β π· β (Metβπ)) & β’ (π β πΉ:ββΆπ) & β’ π½ = (MetOpenβπ·) & β’ πΊ = (π₯ β β β¦ ((πΉβπ₯)π·π)) & β’ (π β π β π) β β’ (π β (πΉ(βπ‘βπ½)π β πΊ β 0)) | ||
Theorem | geomcau 37167* | If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
β’ (π β π· β (Metβπ)) & β’ (π β πΉ:ββΆπ) & β’ (π β π΄ β β) & β’ (π β π΅ β β+) & β’ (π β π΅ < 1) & β’ ((π β§ π β β) β ((πΉβπ)π·(πΉβ(π + 1))) β€ (π΄ Β· (π΅βπ))) β β’ (π β πΉ β (Cauβπ·)) | ||
Theorem | caures 37168 | The restriction of a Cauchy sequence to an upper set of integers is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) & β’ (π β πΉ β (π βpm β)) β β’ (π β (πΉ β (Cauβπ·) β (πΉ βΎ π) β (Cauβπ·))) | ||
Theorem | caushft 37169* | A shifted Cauchy sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) & β’ π = (β€β₯β(π + π)) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = (πΊβ(π + π))) & β’ (π β πΉ β (Cauβπ·)) & β’ (π β πΊ:πβΆπ) β β’ (π β πΊ β (Cauβπ·)) | ||
Theorem | constcncf 37170* | A constant function is a continuous function on β. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved into main set.mm as cncfmptc 24819 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
β’ πΉ = (π₯ β β β¦ π΄) β β’ (π΄ β β β πΉ β (ββcnββ)) | ||
Theorem | cnres2 37171* | The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (πΎ βΎt π΅))) | ||
Theorem | cnresima 37172 | A continuous function is continuous onto its image. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
β’ ((π½ β Top β§ πΎ β Top β§ πΉ β (π½ Cn πΎ)) β πΉ β (π½ Cn (πΎ βΎt ran πΉ))) | ||
Theorem | cncfres 37173* | A continuous function on complex numbers restricted to a subset. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
β’ π΄ β β & β’ π΅ β β & β’ πΉ = (π₯ β β β¦ πΆ) & β’ πΊ = (π₯ β π΄ β¦ πΆ) & β’ (π₯ β π΄ β πΆ β π΅) & β’ πΉ β (ββcnββ) & β’ π½ = (MetOpenβ((abs β β ) βΎ (π΄ Γ π΄))) & β’ πΎ = (MetOpenβ((abs β β ) βΎ (π΅ Γ π΅))) β β’ πΊ β (π½ Cn πΎ) | ||
Syntax | ctotbnd 37174 | Extend class notation with the class of totally bounded metric spaces. |
class TotBnd | ||
Syntax | cbnd 37175 | Extend class notation with the class of bounded metric spaces. |
class Bnd | ||
Definition | df-totbnd 37176* | Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ TotBnd = (π₯ β V β¦ {π β (Metβπ₯) β£ βπ β β+ βπ£ β Fin (βͺ π£ = π₯ β§ βπ β π£ βπ¦ β π₯ π = (π¦(ballβπ)π))}) | ||
Theorem | istotbnd 37177* | The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (TotBndβπ) β (π β (Metβπ) β§ βπ β β+ βπ£ β Fin (βͺ π£ = π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) | ||
Theorem | istotbnd2 37178* | The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (Metβπ) β (π β (TotBndβπ) β βπ β β+ βπ£ β Fin (βͺ π£ = π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) | ||
Theorem | istotbnd3 37179* | A metric space is totally bounded iff there is a finite Ξ΅-net for every positive Ξ΅. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015.) |
β’ (π β (TotBndβπ) β (π β (Metβπ) β§ βπ β β+ βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) | ||
Theorem | totbndmet 37180 | The predicate "totally bounded" implies π is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π β (TotBndβπ) β π β (Metβπ)) | ||
Theorem | 0totbnd 37181 | The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015.) |
β’ (π = β β (π β (TotBndβπ) β π β (Metβπ))) | ||
Theorem | sstotbnd2 37182* | Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015.) |
β’ π = (π βΎ (π Γ π)) β β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ£ β (π« π β© Fin)π β βͺ π₯ β π£ (π₯(ballβπ)π))) | ||
Theorem | sstotbnd 37183* | Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ π = (π βΎ (π Γ π)) β β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ£ β Fin (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) | ||
Theorem | sstotbnd3 37184* | Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ π = (π βΎ (π Γ π)) β β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ£ β π« π(π β βͺ π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β } β Fin))) | ||
Theorem | totbndss 37185 | A subset of a totally bounded metric space is totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β (TotBndβπ) β§ π β π) β (π βΎ (π Γ π)) β (TotBndβπ)) | ||
Theorem | equivtotbnd 37186* | If the metric π is "strongly finer" than π (meaning that there is a positive real constant π such that π(π₯, π¦) β€ π Β· π(π₯, π¦)), then total boundedness of π implies total boundedness of π. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ (π β π β (TotBndβπ)) & β’ (π β π β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π Β· (π₯ππ¦))) β β’ (π β π β (TotBndβπ)) | ||
Definition | df-bnd 37187* | Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ Bnd = (π₯ β V β¦ {π β (Metβπ₯) β£ βπ¦ β π₯ βπ β β+ π₯ = (π¦(ballβπ)π)}) | ||
Theorem | isbnd 37188* | The predicate "is a bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) | ||
Theorem | bndmet 37189 | A bounded metric space is a metric space. (Contributed by Mario Carneiro, 16-Sep-2015.) |
β’ (π β (Bndβπ) β π β (Metβπ)) | ||
Theorem | isbndx 37190* | A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015.) |
β’ (π β (Bndβπ) β (π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) | ||
Theorem | isbnd2 37191* | The predicate "is a bounded metric space". Uses a single point instead of an arbitrary point in the space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π β (Bndβπ) β§ π β β ) β (π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) | ||
Theorem | isbnd3 37192* | A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) | ||
Theorem | isbnd3b 37193* | A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β β βπ¦ β π βπ§ β π (π¦ππ§) β€ π₯)) | ||
Theorem | bndss 37194 | A subset of a bounded metric space is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π β (Bndβπ) β§ π β π) β (π βΎ (π Γ π)) β (Bndβπ)) | ||
Theorem | blbnd 37195 | A ball is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 15-Jan-2014.) |
β’ ((π β (βMetβπ) β§ π β π β§ π β β) β (π βΎ ((π(ballβπ)π ) Γ (π(ballβπ)π ))) β (Bndβ(π(ballβπ)π ))) | ||
Theorem | ssbnd 37196* | A subset of a metric space is bounded iff it is contained in a ball around π, for any π in the larger space. (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ π = (π βΎ (π Γ π)) β β’ ((π β (Metβπ) β§ π β π) β (π β (Bndβπ) β βπ β β π β (π(ballβπ)π))) | ||
Theorem | totbndbnd 37197 | A totally bounded metric space is bounded. This theorem fails for extended metrics - a bounded extended metric is a metric, but there are totally bounded extended metrics that are not metrics (if we were to weaken istotbnd 37177 to only require that π be an extended metric). A counterexample is the discrete extended metric (assigning distinct points distance +β) on a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ (π β (TotBndβπ) β π β (Bndβπ)) | ||
Theorem | equivbnd 37198* | If the metric π is "strongly finer" than π (meaning that there is a positive real constant π such that π(π₯, π¦) β€ π Β· π(π₯, π¦)), then boundedness of π implies boundedness of π. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ (π β π β (Bndβπ)) & β’ (π β π β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π Β· (π₯ππ¦))) β β’ (π β π β (Bndβπ)) | ||
Theorem | bnd2lem 37199 | Lemma for equivbnd2 37200 and similar theorems. (Contributed by Jeff Madsen, 16-Sep-2015.) |
β’ π· = (π βΎ (π Γ π)) β β’ ((π β (Metβπ) β§ π· β (Bndβπ)) β π β π) | ||
Theorem | equivbnd2 37200* | If balls are totally bounded in the metric π, then balls are totally bounded in the equivalent metric π. (Contributed by Mario Carneiro, 15-Sep-2015.) |
β’ (π β π β (Metβπ)) & β’ (π β π β (Metβπ)) & β’ (π β π β β+) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π Β· (π₯ππ¦))) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β€ (π Β· (π₯ππ¦))) & β’ πΆ = (π βΎ (π Γ π)) & β’ π· = (π βΎ (π Γ π)) & β’ (π β (πΆ β (TotBndβπ) β πΆ β (Bndβπ))) β β’ (π β (π· β (TotBndβπ) β π· β (Bndβπ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |