Home | Metamath
Proof Explorer Theorem List (p. 361 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | poimirlem28 36001* | Lemma for poimir 36006, 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 36002* | Lemma for poimir 36006 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 36003* | Lemma for poimir 36006 combining poimirlem29 36002 with bwth 22683. (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 36004* | Lemma for poimir 36006, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 36003 and poimirlem28 36001. 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 36005* | Lemma for poimir 36006, combining poimirlem28 36001, poimirlem30 36003, and poimirlem31 36004 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 36006* | 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 36007* | 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 36008 | 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 36009* | Lemma for ismblfin 36014; could also be used to shorten proof of opnmbllem 24887. (Contributed by Brendan Leahy, 13-Jul-2018.) |
β’ (π΄ β (topGenβran (,)) β βͺ ([,] β {π§ β ran (π₯ β β€, π¦ β β0 β¦ β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) β£ ([,]βπ§) β π΄}) = π΄) | ||
Theorem | mblfinlem1 36010* | Lemma for ismblfin 36014, 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 36011* | Lemma for ismblfin 36014, 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 36012* | The difference between two sets measurable by the criterion in ismblfin 36014 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 36013* | Backward direction of ismblfin 36014. (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 36014* | 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 36015* | ovoliun 24791 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.) |
β’ ((π Fn β β§ βπ β β ((πβπ) β β β§ (vol*β(πβπ)) β β)) β (vol*ββͺ π β β (πβπ)) β€ sup(ran seq1( + , (π β β β¦ (vol*β(πβπ)))), β*, < )) β β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | ex-ovoliunnfl 36016* | Demonstration of ovoliunnfl 36015. (Contributed by Brendan Leahy, 21-Nov-2017.) |
β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | voliunnfl 36017* | voliun 24840 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 36018* | volsup 24842 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 2-Jan-2018.) |
β’ ((π:ββΆdom vol β§ βπ β β (πβπ) β (πβ(π + 1))) β (volββͺ ran π) = sup((vol β ran π), β*, < )) β β’ ((π΄ βΌ β β§ βπ₯ β π΄ π₯ βΌ β) β βͺ π΄ β β) | ||
Theorem | mbfresfi 36019* | Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π β Fin) & β’ (π β βπ β π (πΉ βΎ π ) β MblFn) & β’ (π β βͺ π = π΄) β β’ (π β πΉ β MblFn) | ||
Theorem | mbfposadd 36020* | 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 36021 | 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 36022 | Lemma for dvtan 36023- 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 36023 | Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018.) |
β’ (β D tan) = (π₯ β dom tan β¦ ((cosβπ₯)β-2)) | ||
Theorem | itg2addnclem 36024* | 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 36025* | Lemma for itg2addnc 36027. 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 36026* | Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 36027. (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 36027 | Alternate proof of itg2add 25046 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 24995, 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 10304, 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 36028* | itg2gt0 25047 holds on functions continuous on an open interval in the absence of ax-cc 10304. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.) |
β’ (π β π < π) & β’ (π β πΉ:ββΆ(0[,)+β)) & β’ ((π β§ π₯ β (π(,)π)) β 0 < (πΉβπ₯)) & β’ (π β (πΉ βΎ (π(,)π)) β ((π(,)π)βcnββ)) β β’ (π β 0 < (β«2βπΉ)) | ||
Theorem | ibladdnclem 36029* | Lemma for ibladdnc 36030; cf ibladdlem 25106, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 36027. (Contributed by Brendan Leahy, 31-Oct-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β π· = (π΅ + πΆ)) & β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) & β’ (π β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π΅), π΅, 0))) β β) & β’ (π β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ πΆ), πΆ, 0))) β β) β β’ (π β (β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ π·), π·, 0))) β β) | ||
Theorem | ibladdnc 36030* | Choice-free analogue of itgadd 25111. A measurability hypothesis is necessitated by the loss of mbfadd 24947; 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 36031* | Lemma for itgaddnc 36033; cf. itgaddlem1 25109. (Contributed by Brendan Leahy, 7-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) & β’ ((π β§ π₯ β π΄) β 0 β€ πΆ) β β’ (π β β«π΄(π΅ + πΆ) dπ₯ = (β«π΄π΅ dπ₯ + β«π΄πΆ dπ₯)) | ||
Theorem | itgaddnclem2 36032* | Lemma for itgaddnc 36033; cf. itgaddlem2 25110. (Contributed by Brendan Leahy, 10-Nov-2017.) (Revised by Brendan Leahy, 3-Apr-2018.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) β β’ (π β β«π΄(π΅ + πΆ) dπ₯ = (β«π΄π΅ dπ₯ + β«π΄πΆ dπ₯)) | ||
Theorem | itgaddnc 36033* | Choice-free analogue of itgadd 25111. (Contributed by Brendan Leahy, 11-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β MblFn) β β’ (π β β«π΄(π΅ + πΆ) dπ₯ = (β«π΄π΅ dπ₯ + β«π΄πΆ dπ₯)) | ||
Theorem | iblsubnc 36034* | Choice-free analogue of iblsub 25108. (Contributed by Brendan Leahy, 11-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β MblFn) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β πΏ1) | ||
Theorem | itgsubnc 36035* | Choice-free analogue of itgsub 25112. (Contributed by Brendan Leahy, 11-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ πΆ) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β MblFn) β β’ (π β β«π΄(π΅ β πΆ) dπ₯ = (β«π΄π΅ dπ₯ β β«π΄πΆ dπ₯)) | ||
Theorem | iblabsnclem 36036* | Lemma for iblabsnc 36037; cf. iblabslem 25114. (Contributed by Brendan Leahy, 7-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ πΊ = (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) & β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β πΏ1) & β’ ((π β§ π₯ β π΄) β (πΉβπ΅) β β) β β’ (π β (πΊ β MblFn β§ (β«2βπΊ) β β)) | ||
Theorem | iblabsnc 36037* | Choice-free analogue of iblabs 25115. As with ibladdnc 36030, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β MblFn) β β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β πΏ1) | ||
Theorem | iblmulc2nc 36038* | Choice-free analogue of iblmulc2 25117. (Contributed by Brendan Leahy, 17-Nov-2017.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β πΏ1) | ||
Theorem | itgmulc2nclem1 36039* | Lemma for itgmulc2nc 36041; cf. itgmulc2lem1 25118. (Contributed by Brendan Leahy, 17-Nov-2017.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) & β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β 0 β€ πΆ) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = β«π΄(πΆ Β· π΅) dπ₯) | ||
Theorem | itgmulc2nclem2 36040* | Lemma for itgmulc2nc 36041; cf. itgmulc2lem2 25119. (Contributed by Brendan Leahy, 19-Nov-2017.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) & β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = β«π΄(πΆ Β· π΅) dπ₯) | ||
Theorem | itgmulc2nc 36041* | Choice-free analogue of itgmulc2 25120. (Contributed by Brendan Leahy, 19-Nov-2017.) |
β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β πΏ1) & β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) β β’ (π β (πΆ Β· β«π΄π΅ dπ₯) = β«π΄(πΆ Β· π΅) dπ₯) | ||
Theorem | itgabsnc 36042* | Choice-free analogue of itgabs 25121. (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 36043* | itggt0 25130 holds for continuous functions in the absence of ax-cc 10304. (Contributed by Brendan Leahy, 16-Nov-2017.) |
β’ (π β π < π) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β πΏ1) & β’ ((π β§ π₯ β (π(,)π)) β π΅ β β+) & β’ (π β (π₯ β (π(,)π) β¦ π΅) β ((π(,)π)βcnββ)) β β’ (π β 0 < β«(π(,)π)π΅ dπ₯) | ||
Theorem | ftc1cnnclem 36044* | Lemma for ftc1cnnc 36045; cf. ftc1lem4 25325. The stronger assumptions of ftc1cn 25329 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 36045* | Choice-free proof of ftc1cn 25329. (Contributed by Brendan Leahy, 20-Nov-2017.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β πΉ β πΏ1) β β’ (π β (β D πΊ) = πΉ) | ||
Theorem | ftc1anclem1 36046 | Lemma for ftc1anc 36054- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 24944, but this proof avoids ax-cc 10304. (Contributed by Brendan Leahy, 18-Jun-2018.) |
β’ ((πΉ:π΄βΆβ β§ πΉ β MblFn) β (abs β πΉ) β MblFn) | ||
Theorem | ftc1anclem2 36047* | Lemma for ftc1anc 36054- 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 36048 | Lemma for ftc1anc 36054- 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 36049* | Lemma for ftc1anc 36054. (Contributed by Brendan Leahy, 17-Jun-2018.) |
β’ ((πΉ β dom β«1 β§ πΊ β πΏ1 β§ πΊ:ββΆβ) β (β«2β(π‘ β β β¦ (absβ((πΊβπ‘) β (πΉβπ‘))))) β β) | ||
Theorem | ftc1anclem5 36050* | Lemma for ftc1anc 36054, 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 36051* | Lemma for ftc1anc 36054- 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 36052* | Lemma for ftc1anc 36054. (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 36053* | Lemma for ftc1anc 36054. (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 36054* | ftc1a 25323 holds for functions that obey the triangle inequality in the absence of ax-cc 10304. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.) |
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (π΄(,)π΅) β π·) & β’ (π β π· β β) & β’ (π β πΉ β πΏ1) & β’ (π β πΉ:π·βΆβ) & β’ (π β βπ β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))(absββ«π (πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ(πΉβπ‘)), 0)))) β β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) | ||
Theorem | ftc2nc 36055* | Choice-free proof of ftc2 25330. (Contributed by Brendan Leahy, 19-Jun-2018.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β (β D πΉ) β ((π΄(,)π΅)βcnββ)) & β’ (π β (β D πΉ) β πΏ1) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β β«(π΄(,)π΅)((β D πΉ)βπ‘) dπ‘ = ((πΉβπ΅) β (πΉβπ΄))) | ||
Theorem | asindmre 36056 | Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (π· β© β) = (-1(,)1) | ||
Theorem | dvasin 36057* | Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (β D (arcsin βΎ π·)) = (π₯ β π· β¦ (1 / (ββ(1 β (π₯β2))))) | ||
Theorem | dvacos 36058* | Derivative of arccosine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
β’ π· = (β β ((-β(,]-1) βͺ (1[,)+β))) β β’ (β D (arccos βΎ π·)) = (π₯ β π· β¦ (-1 / (ββ(1 β (π₯β2))))) | ||
Theorem | dvreasin 36059 | 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 36060 | 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 36061* | 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 36062* | 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 36063* | 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 36064* | 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 36065* | 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 36066* | 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 36067* | 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 36068* | 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 36069* | 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 36070* | Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ π = {β¨π₯, π¦β© β£ π} & β’ (π β π΄ β πΆ) β β’ (π΅ β π· β (π΄π π΅ β π)) | ||
Theorem | opelopab3 36071* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ (π β π΄ β πΆ) β β’ (π΅ β π· β (β¨π΄, π΅β© β {β¨π₯, π¦β© β£ π} β π)) | ||
Theorem | cocanfo 36072 | 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 36073 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π΅ β V β β’ (π΄(π βΎ πΆ)π΅ β π΄π π΅) | ||
Theorem | fnopabeqd 36074* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |
β’ (π β π΅ = πΆ) β β’ (π β {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = π΅)} = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = πΆ)}) | ||
Theorem | fvopabf4g 36075* | 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 | eqfnun 36076 | Two functions on π΄ βͺ π΅ are equal if and only if they have equal restrictions to both π΄ and π΅. (Contributed by Jeff Madsen, 19-Jun-2011.) |
β’ ((πΉ Fn (π΄ βͺ π΅) β§ πΊ Fn (π΄ βͺ π΅)) β (πΉ = πΊ β ((πΉ βΎ π΄) = (πΊ βΎ π΄) β§ (πΉ βΎ π΅) = (πΊ βΎ π΅)))) | ||
Theorem | fnopabco 36077* | 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 36078* | Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
β’ (π₯ β π΄ β π΅ β π ) & β’ (π₯ β π΄ β πΆ β π) & β’ πΉ = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = β¨π΅, πΆβ©)} & β’ πΊ = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ = (π΅ππΆ))} β β’ (π Fn (π Γ π) β πΊ = (π β πΉ)) | ||
Theorem | cocnv 36079 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((Fun πΉ β§ Fun πΊ) β ((πΉ β πΊ) β β‘πΊ) = (πΉ βΎ ran πΊ)) | ||
Theorem | f1ocan1fv 36080 | 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 36081 | 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 36082* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (Xπ₯ β π΄ π΅ β© Xπ₯ β π΄ πΆ) = Xπ₯ β π΄ (π΅ β© πΆ) | ||
Theorem | upixp 36083* | 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 36084* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π¦ β π΄ β β*π₯π) β β’ (π΄ β π β {π₯ β£ βπ¦ β π΄ π} βΌ π΄) | ||
Theorem | abrexdom2 36085* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β π β {π₯ β£ βπ¦ β π΄ π₯ = π΅} βΌ π΄) | ||
Theorem | ac6gf 36086* | Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ β²π¦π & β’ (π¦ = (πβπ₯) β (π β π)) β β’ ((π΄ β πΆ β§ βπ₯ β π΄ βπ¦ β π΅ π) β βπ(π:π΄βΆπ΅ β§ βπ₯ β π΄ π)) | ||
Theorem | indexa 36087* | 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 36088* | 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 36089* | A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π Fr π΄ β§ (π΅ β πΆ β§ π΅ β π΄ β§ π΅ β β )) β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΄ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§))) | ||
Theorem | welb 36090* | A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π We π΄ β§ (π΅ β πΆ β§ π΅ β π΄ β§ π΅ β β )) β (β‘π Or π΅ β§ βπ₯ β π΅ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΅ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§)))) | ||
Theorem | supex2g 36091 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β πΆ β sup(π΅, π΄, π ) β V) | ||
Theorem | supclt 36092* | Closure of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π Or π΄ β§ βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β sup(π΅, π΄, π ) β π΄) | ||
Theorem | supubt 36093* | Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π Or π΄ β§ βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β (πΆ β π΅ β Β¬ sup(π΅, π΄, π )π πΆ)) | ||
Theorem | filbcmb 36094* | Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π΄ β Fin β§ π΄ β β β§ π΅ β β) β (βπ₯ β π΄ βπ¦ β π΅ βπ§ β π΅ (π¦ β€ π§ β π) β βπ¦ β π΅ βπ§ β π΅ (π¦ β€ π§ β βπ₯ β π΄ π))) | ||
Theorem | fzmul 36095 | Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β) β (π½ β (π...π) β (πΎ Β· π½) β ((πΎ Β· π)...(πΎ Β· π)))) | ||
Theorem | sdclem2 36096* | Lemma for sdc 36098. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = (β€β₯βπ) & β’ (π = (π βΎ (π...π)) β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π = β β§ π = (π + 1)) β (π β π)) & β’ (π β π΄ β π) & β’ (π β π β β€) & β’ (π β βπ(π:{π}βΆπ΄ β§ π)) & β’ ((π β§ π β π) β ((π:(π...π)βΆπ΄ β§ π) β ββ(β:(π...(π + 1))βΆπ΄ β§ π = (β βΎ (π...π)) β§ π))) & β’ π½ = {π β£ βπ β π (π:(π...π)βΆπ΄ β§ π)} & β’ πΉ = (π€ β π, π₯ β π½ β¦ {β β£ βπ β π (β:(π...(π + 1))βΆπ΄ β§ π₯ = (β βΎ (π...π)) β§ π)}) & β’ β²ππ & β’ (π β πΊ:πβΆπ½) & β’ (π β (πΊβπ):(π...π)βΆπ΄) & β’ ((π β§ π€ β π) β (πΊβ(π€ + 1)) β (π€πΉ(πΊβπ€))) β β’ (π β βπ(π:πβΆπ΄ β§ βπ β π π)) | ||
Theorem | sdclem1 36097* | Lemma for sdc 36098. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = (β€β₯βπ) & β’ (π = (π βΎ (π...π)) β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π = β β§ π = (π + 1)) β (π β π)) & β’ (π β π΄ β π) & β’ (π β π β β€) & β’ (π β βπ(π:{π}βΆπ΄ β§ π)) & β’ ((π β§ π β π) β ((π:(π...π)βΆπ΄ β§ π) β ββ(β:(π...(π + 1))βΆπ΄ β§ π = (β βΎ (π...π)) β§ π))) & β’ π½ = {π β£ βπ β π (π:(π...π)βΆπ΄ β§ π)} & β’ πΉ = (π€ β π, π₯ β π½ β¦ {β β£ βπ β π (β:(π...(π + 1))βΆπ΄ β§ π₯ = (β βΎ (π...π)) β§ π)}) β β’ (π β βπ(π:πβΆπ΄ β§ βπ β π π)) | ||
Theorem | sdc 36098* | 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 36099* | 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 36100* | Variant of fdc 36099 with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010.) |
β’ π΄ β V & β’ π β β€ & β’ π = (β€β₯βπ) & β’ π = (π + 1) & β’ (π = (πβπ) β (π β π)) & β’ (π = (πβ(π β 1)) β (π β π)) & β’ (π = (πβπ) β (π β π)) & β’ (π = (πβπ) β (π β π)) & β’ (π β βπ β π΄ π) & β’ (π β π Fr π΄) & β’ ((π β§ π β π΄) β (π β¨ βπ β π΄ π)) & β’ (((π β§ π) β§ (π β π΄ β§ π β π΄)) β ππ π) β β’ (π β βπ β π βπ(π:(π...π)βΆπ΄ β§ (π β§ π) β§ βπ β (π...π)π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |