![]() |
Metamath
Proof Explorer Theorem List (p. 366 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | poimirlem18 36501* | Lemma for poimir 36516 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.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) & β’ (π β (2nd βπ) = 0) β β’ (π β β!π§ β π π§ β π) | ||
Theorem | poimirlem19 36502* | Lemma for poimir 36516 establishing the vertices of the simplex in poimirlem20 36503. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) & β’ (π β (2nd βπ) = π) β β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ ((π β (1...π) β¦ (((1st β(1st βπ))βπ) β if(π = ((2nd β(1st βπ))βπ), 1, 0))) βf + (((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = 1, π, (π β 1)))) β (1...(π¦ + 1))) Γ {1}) βͺ ((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = 1, π, (π β 1)))) β (((π¦ + 1) + 1)...π)) Γ {0}))))) | ||
Theorem | poimirlem20 36503* | Lemma for poimir 36516 establishing existence for poimirlem21 36504. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) & β’ (π β (2nd βπ) = π) β β’ (π β βπ§ β π π§ β π) | ||
Theorem | poimirlem21 36504* | Lemma for poimir 36516 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.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) & β’ (π β (2nd βπ) = π) β β’ (π β β!π§ β π π§ β π) | ||
Theorem | poimirlem22 36505* | Lemma for poimir 36516, 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.) |
β’ (π β π β β) & β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st β(1st βπ‘)) βf + ((((2nd β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} & β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) & β’ (π β π β π) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) & β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) β β’ (π β β!π§ β π π§ β π) | ||
Theorem | poimirlem23 36506* | Lemma for poimir 36516, 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.) |
β’ (π β π β β) & β’ (π β π:(1...π)βΆ(0..^πΎ)) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) & β’ (π β π β (0...π)) β β’ (π β (βπ β ran (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))))(πβπ) β 0 β Β¬ (π = π β§ ((πβπ) = 0 β§ (πβπ) = π)))) | ||
Theorem | poimirlem24 36507* | Lemma for poimir 36516, 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.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) & β’ (π β π:(1...π)βΆ(0..^πΎ)) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) & β’ (π β π β (0...π)) β β’ (π β (βπ₯ β (((0...πΎ) βm (1...π)) βm (0...(π β 1)))(π₯ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) β§ ((0...(π β 1)) β ran (π β ran π₯ β¦ π΅) β§ βπ β ran π₯(πβπ) β 0)) β (βπ β (0...(π β 1))βπ β ((0...π) β {π})π = β¦β¨π, πβ© / π β¦πΆ β§ Β¬ (π = π β§ ((πβπ) = 0 β§ (πβπ) = π))))) | ||
Theorem | poimirlem25 36508* | Lemma for poimir 36516 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.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) & β’ (π β π:(1...π)βΆ(0..^πΎ)) & β’ (π β π:(1...π)β1-1-ontoβ(1...π)) & β’ ((π β§ π β (0...π)) β π β β¦β¨π, πβ© / π β¦πΆ) β β’ (π β 2 β₯ (β―β{π¦ β (0...π) β£ βπ β (0...(π β 1))βπ β ((0...π) β {π¦})π = β¦β¨π, πβ© / π β¦πΆ})) | ||
Theorem | poimirlem26 36509* | Lemma for poimir 36516 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.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) β β’ (π β 2 β₯ ((β―β{π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ βπ β (0...(π β 1))βπ β ((0...π) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦πΆ}) β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ}))) | ||
Theorem | poimirlem27 36510* | Lemma for poimir 36516 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.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) & β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β π΅ < π) & β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = πΎ)) β π΅ β (π β 1)) β β’ (π β 2 β₯ ((β―β{π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ βπ β (0...(π β 1))βπ β ((0...π) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦πΆ}) β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (βπ β (0...(π β 1))βπ β (0...(π β 1))π = πΆ β§ ((1st βπ )βπ) = 0 β§ ((2nd βπ )βπ) = π)}))) | ||
Theorem | poimirlem28 36511* | Lemma for poimir 36516, a variant of Sperner's lemma. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ (π = ((1st βπ ) βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) & β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) & β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β π΅ < π) & β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = πΎ)) β π΅ β (π β 1)) & β’ (π β πΎ β β) β β’ (π β βπ β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})βπ β (0...π)βπ β (0...π)π = πΆ) | ||
Theorem | poimirlem29 36512* | Lemma for poimir 36516 connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ π = ((πΉβ(((1st β(πΊβπ)) βf + ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf / ((1...π) Γ {π})))βπ) & β’ (π β πΊ:ββΆ((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) & β’ ((π β§ π β β) β ran (1st β(πΊβπ)) β (0..^π)) & β’ ((π β§ (π β β β§ π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0ππ) β β’ (π β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ (β Γ β)))(1 / π)) β βπ β (1...π)βπ£ β (π βΎt πΌ)(πΆ β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) | ||
Theorem | poimirlem30 36513* | Lemma for poimir 36516 combining poimirlem29 36512 with bwth 22913. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ π = ((πΉβ(((1st β(πΊβπ)) βf + ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf / ((1...π) Γ {π})))βπ) & β’ (π β πΊ:ββΆ((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) & β’ ((π β§ π β β) β ran (1st β(πΊβπ)) β (0..^π)) & β’ ((π β§ (π β β β§ π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0ππ) β β’ (π β βπ β πΌ βπ β (1...π)βπ£ β (π βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) | ||
Theorem | poimirlem31 36514* | Lemma for poimir 36516, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 36513 and poimirlem28 36511. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) & β’ π = ((1st β(πΊβπ)) βf + ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) & β’ (π β πΊ:ββΆ((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) & β’ ((π β§ π β β) β ran (1st β(πΊβπ)) β (0..^π)) & β’ ((π β§ (π β β β§ π β (0...π))) β βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < )) β β’ ((π β§ (π β β β§ π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0π((πΉβ(π βf / ((1...π) Γ {π})))βπ)) | ||
Theorem | poimirlem32 36515* | Lemma for poimir 36516, combining poimirlem28 36511, poimirlem30 36513, and poimirlem31 36514 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ ((πΉβπ§)βπ)) β β’ (π β βπ β πΌ βπ β (1...π)βπ£ β (π βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) | ||
Theorem | poimir 36516* | Poincare-Miranda theorem. Theorem on [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn π )) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) & β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ ((πΉβπ§)βπ)) β β’ (π β βπ β πΌ (πΉβπ) = ((1...π) Γ {0})) | ||
Theorem | broucube 36517* | 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.) |
β’ (π β π β β) & β’ πΌ = ((0[,]1) βm (1...π)) & β’ π = (βtβ((1...π) Γ {(topGenβran (,))})) & β’ (π β πΉ β ((π βΎt πΌ) Cn (π βΎt πΌ))) β β’ (π β βπ β πΌ π = (πΉβπ)) | ||
Theorem | heicant 36518 | 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.) |
β’ (π β πΆ β (βMetβπ)) & β’ (π β π· β (βMetβπ)) & β’ (π β (MetOpenβπΆ) β Comp) & β’ (π β π β β ) & β’ (π β π β β ) β β’ (π β ((metUnifβπΆ) Cnu(metUnifβπ·)) = ((MetOpenβπΆ) Cn (MetOpenβπ·))) | ||
Theorem | opnmbllem0 36519* | Lemma for ismblfin 36524; could also be used to shorten proof of opnmbllem 25117. (Contributed by Brendan Leahy, 13-Jul-2018.) |
β’ (π΄ β (topGenβran (,)) β βͺ ([,] β {π§ β ran (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β£ ([,]βπ§) β π΄}) = π΄) | ||
Theorem | mblfinlem1 36520* | Lemma for ismblfin 36524, 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.) |
β’ ((π΄ β (topGenβran (,)) β§ π΄ β β ) β βπ π:ββ1-1-ontoβ{π β {π β ran (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β£ ([,]βπ) β π΄} β£ βπ β {π β ran (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β£ ([,]βπ) β π΄} (([,]βπ) β ([,]βπ) β π = π)}) | ||
Theorem | mblfinlem2 36521* | Lemma for ismblfin 36524, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different definition 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.) |
β’ ((π΄ β (topGenβran (,)) β§ π β β β§ π < (vol*βπ΄)) β βπ β (Clsdβ(topGenβran (,)))(π β π΄ β§ π < (vol*βπ ))) | ||
Theorem | mblfinlem3 36522* | The difference between two sets measurable by the criterion in ismblfin 36524 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.) |
β’ (((π΄ β β β§ (vol*βπ΄) β β) β§ (π΅ β β β§ (vol*βπ΅) β β) β§ ((vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ) β§ (vol*βπ΅) = sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β π΅ β§ π¦ = (volβπ))}, β, < ))) β sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β (π΄ β π΅) β§ π¦ = (volβπ))}, β, < ) = (vol*β(π΄ β π΅))) | ||
Theorem | mblfinlem4 36523* | Backward direction of ismblfin 36524. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
β’ (((π΄ β β β§ (vol*βπ΄) β β) β§ π΄ β dom vol) β (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) | ||
Theorem | ismblfin 36524* | 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.) |
β’ ((π΄ β β β§ (vol*βπ΄) β β) β (π΄ β dom vol β (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ))) | ||
Theorem | ovoliunnfl 36525* | ovoliun 25021 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.) |
β’ ((π Fn β β§ βπ β β ((πβπ) β β β§ (vol*β(πβπ)) β β)) β (vol*ββͺ π β β (πβπ)) β€ sup(ran seq1( + , (π β β β¦ (vol*β(πβπ)))), β*, < )) β β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | ex-ovoliunnfl 36526* | Demonstration of ovoliunnfl 36525. (Contributed by Brendan Leahy, 21-Nov-2017.) |
β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | voliunnfl 36527* | voliun 25070 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.) |
β’ π = seq1( + , πΊ) & β’ πΊ = (π β β β¦ (volβ(πβπ))) & β’ ((βπ β β ((πβπ) β dom vol β§ (volβ(πβπ)) β β) β§ Disj π β β (πβπ)) β (volββͺ π β β (πβπ)) = sup(ran π, β*, < )) β β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | volsupnfl 36528* | volsup 25072 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.) |
β’ ((π:ββΆdom vol β§ βπ β β (πβπ) β (πβ(π + 1))) β (volββͺ ran π) = sup((vol β ran π), β*, < )) β β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | mbfresfi 36529* | Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π β Fin) & β’ (π β βπ β π (πΉ βΎ π ) β MblFn) & β’ (π β βͺ π = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfposadd 36530* | 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) β β’ (π β (π₯ β π΄ β¦ (if(0 β€ π΅, π΅, 0) + if(0 β€ πΆ, πΆ, 0))) β MblFn) | ||
Theorem | cnambfre 36531 | A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018.) |
β’ ((πΉ:π΄βΆβ β§ π΄ β dom vol β§ (vol*β(π΄ β ((β‘(((topGenβran (,)) βΎt π΄) CnP (topGenβran (,))) β E ) β {πΉ}))) = 0) β πΉ β MblFn) | ||
Theorem | dvtanlem 36532 | Lemma for dvtan 36533- the domain of the tangent is open. (Contributed by Brendan Leahy, 8-Aug-2018.) (Proof shortened by OpenAI, 3-Jul-2020.) |
β’ (β‘cos β (β β {0})) β (TopOpenββfld) | ||
Theorem | dvtan 36533 | Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.) |
β’ (β D tan) = (π₯ β dom tan β¦ ((cosβπ₯)β-2)) | ||
Theorem | itg2addnclem 36534* | An alternate expression for the β«2 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.) |
β’ πΏ = {π₯ β£ βπ β dom β«1(βπ¦ β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π¦))) βr β€ πΉ β§ π₯ = (β«1βπ))} β β’ (πΉ:ββΆ(0[,]+β) β (β«2βπΉ) = sup(πΏ, β*, < )) | ||
Theorem | itg2addnclem2 36535* | Lemma for itg2addnc 36537. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) β β’ (((π β§ β β dom β«1) β§ π£ β β+) β (π₯ β β β¦ if(((((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)) β€ (ββπ₯) β§ (ββπ₯) β 0), (((ββ((πΉβπ₯) / (π£ / 3))) β 1) Β· (π£ / 3)), (ββπ₯))) β dom β«1) | ||
Theorem | itg2addnclem3 36536* | Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 36537. (Contributed by Brendan Leahy, 11-Mar-2018.) |
β’ (π β πΉ β MblFn) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΊ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΊ) β β) β β’ (π β (ββ β dom β«1(βπ¦ β β+ (π§ β β β¦ if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ)) β βπ‘βπ’(βπ β dom β«1βπ β dom β«1((βπ β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’)))) | ||
Theorem | itg2addnc 36537 | Alternate proof of itg2add 25276 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 25225, 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 10429, 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) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΉ) β β) & β’ (π β πΊ:ββΆ(0[,)+β)) & β’ (π β (β«2βπΊ) β β) β β’ (π β (β«2β(πΉ βf + πΊ)) = ((β«2βπΉ) + (β«2βπΊ))) | ||
Theorem | itg2gt0cn 36538* | itg2gt0 25277 holds on functions continuous on an open interval in the absence of ax-cc 10429. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.) |
β’ (π β π < π) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ ((π β§ π₯ β (π(,)π)) β 0 < (πΉβπ₯)) & β’ (π β (πΉ βΎ (π(,)π)) β ((π(,)π)βcnββ)) β β’ (π β 0 < (β«2βπΉ)) | ||
Theorem | ibladdnclem 36539* | Lemma for ibladdnc 36540; cf ibladdlem 25336, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 36537. (Contributed by Brendan Leahy, 31-Oct-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β π· = (π΅ + πΆ)) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ (π β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π΅), π΅, 0))) β β) & β’ (π β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ πΆ), πΆ, 0))) β β) β β’ (π β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π·), π·, 0))) β β) | ||
Theorem | ibladdnc 36540* | Choice-free analogue of itgadd 25341. A measurability hypothesis is necessitated by the loss of mbfadd 25177; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β πΏ1) | ||
Theorem | itgaddnclem1 36541* | Lemma for itgaddnc 36543; cf. itgaddlem1 25339. (Contributed by Brendan Leahy, 7-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) & β’ ((π β§ π₯ β π΄) β 0 β€ πΆ) β β’ (π β β«π΄(π΅ + πΆ) dπ₯ = (β«π΄π΅ dπ₯ + β«π΄πΆ dπ₯)) | ||
Theorem | itgaddnclem2 36542* | Lemma for itgaddnc 36543; cf. itgaddlem2 25340. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) β β’ (π β β«π΄(π΅ + πΆ) dπ₯ = (β«π΄π΅ dπ₯ + β«π΄πΆ dπ₯)) | ||
Theorem | itgaddnc 36543* | Choice-free analogue of itgadd 25341. (Contributed by Brendan Leahy, 11-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) β β’ (π β β«π΄(π΅ + πΆ) dπ₯ = (β«π΄π΅ dπ₯ + β«π΄πΆ dπ₯)) | ||
Theorem | iblsubnc 36544* | Choice-free analogue of iblsub 25338. (Contributed by Brendan Leahy, 11-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β MblFn) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β πΏ1) | ||
Theorem | itgsubnc 36545* | Choice-free analogue of itgsub 25342. (Contributed by Brendan Leahy, 11-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β MblFn) β β’ (π β β«π΄(π΅ β πΆ) dπ₯ = (β«π΄π΅ dπ₯ β β«π΄πΆ dπ₯)) | ||
Theorem | iblabsnclem 36546* | Lemma for iblabsnc 36547; cf. iblabslem 25344. (Contributed by Brendan Leahy, 7-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ πΊ = (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) & β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β πΏ1) & β’ ((π β§ π₯ β π΄) β (πΉβπ΅) β β) β β’ (π β (πΊ β MblFn β§ (β«2βπΊ) β β)) | ||
Theorem | iblabsnc 36547* | Choice-free analogue of iblabs 25345. As with ibladdnc 36540, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β MblFn) β β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β πΏ1) | ||
Theorem | iblmulc2nc 36548* | Choice-free analogue of iblmulc2 25347. (Contributed by Brendan Leahy, 17-Nov-2017.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β πΏ1) | ||
Theorem | itgmulc2nclem1 36549* | Lemma for itgmulc2nc 36551; cf. itgmulc2lem1 25348. (Contributed by Brendan Leahy, 17-Nov-2017.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) & β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β 0 β€ πΆ) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = β«π΄(πΆ Β· π΅) dπ₯) | ||
Theorem | itgmulc2nclem2 36550* | Lemma for itgmulc2nc 36551; cf. itgmulc2lem2 25349. (Contributed by Brendan Leahy, 19-Nov-2017.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) & β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = β«π΄(πΆ Β· π΅) dπ₯) | ||
Theorem | itgmulc2nc 36551* | Choice-free analogue of itgmulc2 25350. (Contributed by Brendan Leahy, 19-Nov-2017.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) β β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = β«π΄(πΆ Β· π΅) dπ₯) | ||
Theorem | itgabsnc 36552* | Choice-free analogue of itgabs 25351. (Contributed by Brendan Leahy, 19-Nov-2017.) (Revised by Brendan Leahy, 19-Jun-2018.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β MblFn) & β’ (π β (π¦ β π΄ β¦ ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) β MblFn) β β’ (π β (absββ«π΄π΅ dπ₯) β€ β«π΄(absβπ΅) dπ₯) | ||
Theorem | itggt0cn 36553* | itggt0 25360 holds for continuous functions in the absence of ax-cc 10429. (Contributed by Brendan Leahy, 16-Nov-2017.) |
β’ (π β π < π) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β β+) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ)) β β’ (π β 0 < β«(π(,)π)π΅ dπ₯) | ||
Theorem | ftc1cnnclem 36554* | Lemma for ftc1cnnc 36555; cf. ftc1lem4 25555. The stronger assumptions of ftc1cn 25559 are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΉ β πΏ1) & β’ (π β π β (π΄(,)π΅)) & β’ π» = (π§ β ((π΄[,]π΅) β {π}) β¦ (((πΊβπ§) β (πΊβπ)) / (π§ β π))) & β’ (π β πΈ β β+) & β’ (π β π β β+) & β’ ((π β§ π¦ β (π΄(,)π΅)) β ((absβ(π¦ β π)) < π β (absβ((πΉβπ¦) β (πΉβπ))) < πΈ)) & β’ (π β π β (π΄[,]π΅)) & β’ (π β (absβ(π β π)) < π ) & β’ (π β π β (π΄[,]π΅)) & β’ (π β (absβ(π β π)) < π ) β β’ ((π β§ π < π) β (absβ((((πΊβπ) β (πΊβπ)) / (π β π)) β (πΉβπ))) < πΈ) | ||
Theorem | ftc1cnnc 36555* | Choice-free proof of ftc1cn 25559. (Contributed by Brendan Leahy, 20-Nov-2017.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΉ β πΏ1) β β’ (π β (β D πΊ) = πΉ) | ||
Theorem | ftc1anclem1 36556 | Lemma for ftc1anc 36564- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 25174, but this proof avoids ax-cc 10429. (Contributed by Brendan Leahy, 18-Jun-2018.) |
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β (abs β πΉ) β MblFn) | ||
Theorem | ftc1anclem2 36557* | Lemma for ftc1anc 36564- 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 36558 | Lemma for ftc1anc 36564- 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 36559* | Lemma for ftc1anc 36564. (Contributed by Brendan Leahy, 17-Jun-2018.) |
β’ ((πΉ β dom β«1 β§ πΊ β πΏ1 β§ πΊ:ββΆβ) β (β«2β(π‘ β β β¦ (absβ((πΊβπ‘) β (πΉβπ‘))))) β β) | ||
Theorem | ftc1anclem5 36560* | Lemma for ftc1anc 36564, 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 36561* | Lemma for ftc1anc 36564- 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 36562* | Lemma for ftc1anc 36564. (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 36563* | Lemma for ftc1anc 36564. (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 36564* | ftc1a 25553 holds for functions that obey the triangle inequality in the absence of ax-cc 10429. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) & β’ (π β βπ β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))(absββ«π (πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ(πΉβπ‘)), 0)))) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | ftc2nc 36565* | Choice-free proof of ftc2 25560. (Contributed by Brendan Leahy, 19-Jun-2018.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (β D πΉ) β ((π΄(,)π΅)βcnββ)) & β’ (π β (β D πΉ) β πΏ1) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | asindmre 36566 | Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (π· β© β) = (-1(,)1) | ||
Theorem | dvasin 36567* | Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (β D (arcsin βΎ π·)) = (π₯ β π· β¦ (1 / (ββ(1 β (π₯β2))))) | ||
Theorem | dvacos 36568* | Derivative of arccosine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (β D (arccos βΎ π·)) = (π₯ β π· β¦ (-1 / (ββ(1 β (π₯β2))))) | ||
Theorem | dvreasin 36569 | 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 36570 | 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 36571* | 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 36572* | 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 36573* | 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 36574* | 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 36575* | 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 36576* | 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 36577* | 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 36578* | 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 36579* | 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 36580* | Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ π = {β¨π₯, π¦β© β£ π} & β’ (π β π΄ β πΆ) β β’ (π΅ β π· β (π΄π π΅ β π)) | ||
Theorem | opelopab3 36581* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ (π β π΄ β πΆ) β β’ (π΅ β π· β (β¨π΄, π΅β© β {β¨π₯, π¦β© β£ π} β π)) | ||
Theorem | cocanfo 36582 | 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 36583 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π΅ β V β β’ (π΄(π βΎ πΆ)π΅ β π΄π π΅) | ||
Theorem | fnopabeqd 36584* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |
β’ (π β π΅ = πΆ) β β’ (π β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = π΅)} = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = πΆ)}) | ||
Theorem | fvopabf4g 36585* | 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 36586* | 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 36587* | Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
β’ (π₯ β π΄ β π΅ β π ) & β’ (π₯ β π΄ β πΆ β π) & β’ πΉ = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = β¨π΅, πΆβ©)} & β’ πΊ = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = (π΅ππΆ))} β β’ (π Fn (π Γ π) β πΊ = (π β πΉ)) | ||
Theorem | cocnv 36588 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((Fun πΉ β§ Fun πΊ) β ((πΉ β πΊ) β β‘πΊ) = (πΉ βΎ ran πΊ)) | ||
Theorem | f1ocan1fv 36589 | 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 36590 | 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 36591* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (Xπ₯ β π΄ π΅ β© Xπ₯ β π΄ πΆ) = Xπ₯ β π΄ (π΅ β© πΆ) | ||
Theorem | upixp 36592* | 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 36593* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π¦ β π΄ β β*π₯π) β β’ (π΄ β π β {π₯ β£ βπ¦ β π΄ π} βΌ π΄) | ||
Theorem | abrexdom2 36594* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β π β {π₯ β£ βπ¦ β π΄ π₯ = π΅} βΌ π΄) | ||
Theorem | ac6gf 36595* | Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ β²π¦π & β’ (π¦ = (πβπ₯) β (π β π)) β β’ ((π΄ β πΆ β§ βπ₯ β π΄ βπ¦ β π΅ π) β βπ(π:π΄βΆπ΅ β§ βπ₯ β π΄ π)) | ||
Theorem | indexa 36596* | 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 36597* | 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 36598* | A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π Fr π΄ β§ (π΅ β πΆ β§ π΅ β π΄ β§ π΅ β β )) β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΄ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§))) | ||
Theorem | welb 36599* | A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π We π΄ β§ (π΅ β πΆ β§ π΅ β π΄ β§ π΅ β β )) β (β‘π Or π΅ β§ βπ₯ β π΅ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΅ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§)))) | ||
Theorem | supex2g 36600 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β πΆ β sup(π΅, π΄, π ) β V) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |