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