![]() |
Metamath
Proof Explorer Theorem List (p. 254 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 | itgvallem 25301* | Substitution lemma. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข (iโ๐พ) = ๐ โ โข (๐ = ๐พ โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / ๐))), (โโ(๐ต / ๐)), 0)))) | ||
Theorem | itgvallem3 25302* | Lemma for itgposval 25312 and itgreval 25313. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต = 0) โ โข (๐ โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) = 0) | ||
Theorem | ibl0 25303 | The zero function is integrable on any measurable set. (Unlike iblconst 25334, this does not require ๐ด to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.) |
โข (๐ด โ dom vol โ (๐ด ร {0}) โ ๐ฟ1) | ||
Theorem | iblcnlem1 25304* | Lemma for iblcnlem 25305. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ ((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง (๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)))) | ||
Theorem | iblcnlem 25305* | Expand out the universal quantifier in isibl2 25283. (Contributed by Mario Carneiro, 6-Aug-2014.) |
โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) โ โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ ((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง (๐ โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)))) | ||
Theorem | itgcnlem 25306* | Expand out the sum in dfitg 25286. (Contributed by Mario Carneiro, 1-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) & โข ๐ = (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ โซ๐ด๐ต d๐ฅ = ((๐ โ ๐) + (i ยท (๐ โ ๐)))) | ||
Theorem | iblrelem 25307* | Integrability of a real function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ ((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ โ โง (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))) โ โ))) | ||
Theorem | iblposlem 25308* | Lemma for iblpos 25309. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) โ โข (๐ โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))) = 0) | ||
Theorem | iblpos 25309* | Integrability of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) โ โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ ((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ))) | ||
Theorem | iblre 25310* | Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ ((๐ฅ โ ๐ด โฆ if(0 โค ๐ต, ๐ต, 0)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ if(0 โค -๐ต, -๐ต, 0)) โ ๐ฟ1))) | ||
Theorem | itgrevallem1 25311* | Lemma for itgposval 25312 and itgreval 25313. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ โซ๐ด๐ต d๐ฅ = ((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -๐ต), -๐ต, 0))))) | ||
Theorem | itgposval 25312* | The integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) โ โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) | ||
Theorem | itgreval 25313* | Decompose the integral of a real function into positive and negative parts. (Contributed by Mario Carneiro, 31-Jul-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ๐ดif(0 โค ๐ต, ๐ต, 0) d๐ฅ โ โซ๐ดif(0 โค -๐ต, -๐ต, 0) d๐ฅ)) | ||
Theorem | itgrecl 25314* | Real closure of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ โซ๐ด๐ต d๐ฅ โ โ) | ||
Theorem | iblcn 25315* | Integrability of a complex function. (Contributed by Mario Carneiro, 6-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1))) | ||
Theorem | itgcnval 25316* | Decompose the integral of a complex function into real and imaginary parts. (Contributed by Mario Carneiro, 6-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) | ||
Theorem | itgre 25317* | Real part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ (โโโซ๐ด๐ต d๐ฅ) = โซ๐ด(โโ๐ต) d๐ฅ) | ||
Theorem | itgim 25318* | Imaginary part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ (โโโซ๐ด๐ต d๐ฅ) = โซ๐ด(โโ๐ต) d๐ฅ) | ||
Theorem | iblneg 25319* | The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ (๐ฅ โ ๐ด โฆ -๐ต) โ ๐ฟ1) | ||
Theorem | itgneg 25320* | Negation of an integral. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ -โซ๐ด๐ต d๐ฅ = โซ๐ด-๐ต d๐ฅ) | ||
Theorem | iblss 25321* | A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ด โ dom vol) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) | ||
Theorem | iblss2 25322* | Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ต โ dom vol) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) & โข ((๐ โง ๐ฅ โ (๐ต โ ๐ด)) โ ๐ถ = 0) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ (๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1) | ||
Theorem | itgitg2 25323* | Transfer an integral using โซ2 to an equivalent integral using โซ. (Contributed by Mario Carneiro, 6-Aug-2014.) |
โข ((๐ โง ๐ฅ โ โ) โ ๐ด โ โ) & โข ((๐ โง ๐ฅ โ โ) โ 0 โค ๐ด) & โข (๐ โ (๐ฅ โ โ โฆ ๐ด) โ ๐ฟ1) โ โข (๐ โ โซโ๐ด d๐ฅ = (โซ2โ(๐ฅ โ โ โฆ ๐ด))) | ||
Theorem | i1fibl 25324 | A simple function is integrable. (Contributed by Mario Carneiro, 6-Aug-2014.) |
โข (๐น โ dom โซ1 โ ๐น โ ๐ฟ1) | ||
Theorem | itgitg1 25325* | Transfer an integral using โซ1 to an equivalent integral using โซ. (Contributed by Mario Carneiro, 6-Aug-2014.) |
โข (๐น โ dom โซ1 โ โซโ(๐นโ๐ฅ) d๐ฅ = (โซ1โ๐น)) | ||
Theorem | itgle 25326* | Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.) |
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โค ๐ถ) โ โข (๐ โ โซ๐ด๐ต d๐ฅ โค โซ๐ด๐ถ d๐ฅ) | ||
Theorem | itgge0 25327* | The integral of a positive function is positive. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) โ โข (๐ โ 0 โค โซ๐ด๐ต d๐ฅ) | ||
Theorem | itgss 25328* | Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข (๐ โ ๐ด โ ๐ต) & โข ((๐ โง ๐ฅ โ (๐ต โ ๐ด)) โ ๐ถ = 0) โ โข (๐ โ โซ๐ด๐ถ d๐ฅ = โซ๐ต๐ถ d๐ฅ) | ||
Theorem | itgss2 25329* | Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014.) |
โข (๐ด โ ๐ต โ โซ๐ด๐ถ d๐ฅ = โซ๐ตif(๐ฅ โ ๐ด, ๐ถ, 0) d๐ฅ) | ||
Theorem | itgeqa 25330* | Approximate equality of integrals. If ๐ถ(๐ฅ) = ๐ท(๐ฅ) for almost all ๐ฅ, then โซ๐ต๐ถ(๐ฅ) d๐ฅ = โซ๐ต๐ท(๐ฅ) d๐ฅ and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Mario Carneiro, 2-Sep-2014.) |
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ท โ โ) & โข (๐ โ ๐ด โ โ) & โข (๐ โ (vol*โ๐ด) = 0) & โข ((๐ โง ๐ฅ โ (๐ต โ ๐ด)) โ ๐ถ = ๐ท) โ โข (๐ โ (((๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1 โ (๐ฅ โ ๐ต โฆ ๐ท) โ ๐ฟ1) โง โซ๐ต๐ถ d๐ฅ = โซ๐ต๐ท d๐ฅ)) | ||
Theorem | itgss3 25331* | Expand the set of an integral by a nullset. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Mario Carneiro, 2-Sep-2014.) |
โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ต โ โ) & โข (๐ โ (vol*โ(๐ต โ ๐ด)) = 0) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ โ) โ โข (๐ โ (((๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1 โ (๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1) โง โซ๐ด๐ถ d๐ฅ = โซ๐ต๐ถ d๐ฅ)) | ||
Theorem | itgioo 25332* | Equality of integrals on open and closed intervals. (Contributed by Mario Carneiro, 2-Sep-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข ((๐ โง ๐ฅ โ (๐ด[,]๐ต)) โ ๐ถ โ โ) โ โข (๐ โ โซ(๐ด(,)๐ต)๐ถ d๐ฅ = โซ(๐ด[,]๐ต)๐ถ d๐ฅ) | ||
Theorem | itgless 25333* | Expand the integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Aug-2014.) |
โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ด โ dom vol) & โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ต) โ 0 โค ๐ถ) & โข (๐ โ (๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ โซ๐ด๐ถ d๐ฅ โค โซ๐ต๐ถ d๐ฅ) | ||
Theorem | iblconst 25334 | A constant function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
โข ((๐ด โ dom vol โง (volโ๐ด) โ โ โง ๐ต โ โ) โ (๐ด ร {๐ต}) โ ๐ฟ1) | ||
Theorem | itgconst 25335* | Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014.) |
โข ((๐ด โ dom vol โง (volโ๐ด) โ โ โง ๐ต โ โ) โ โซ๐ด๐ต d๐ฅ = (๐ต ยท (volโ๐ด))) | ||
Theorem | ibladdlem 25336* | Lemma for ibladd 25337. (Contributed by Mario Carneiro, 17-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ท = (๐ต + ๐ถ)) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ MblFn) & โข (๐ โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ต), ๐ต, 0))) โ โ) & โข (๐ โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ถ), ๐ถ, 0))) โ โ) โ โข (๐ โ (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค ๐ท), ๐ท, 0))) โ โ) | ||
Theorem | ibladd 25337* | Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ต + ๐ถ)) โ ๐ฟ1) | ||
Theorem | iblsub 25338* | Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ต โ ๐ถ)) โ ๐ฟ1) | ||
Theorem | itgaddlem1 25339* | Lemma for itgadd 25341. (Contributed by Mario Carneiro, 17-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) & โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ถ) โ โข (๐ โ โซ๐ด(๐ต + ๐ถ) d๐ฅ = (โซ๐ด๐ต d๐ฅ + โซ๐ด๐ถ d๐ฅ)) | ||
Theorem | itgaddlem2 25340* | Lemma for itgadd 25341. (Contributed by Mario Carneiro, 17-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) โ โข (๐ โ โซ๐ด(๐ต + ๐ถ) d๐ฅ = (โซ๐ด๐ต d๐ฅ + โซ๐ด๐ถ d๐ฅ)) | ||
Theorem | itgadd 25341* | Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ โซ๐ด(๐ต + ๐ถ) d๐ฅ = (โซ๐ด๐ต d๐ฅ + โซ๐ด๐ถ d๐ฅ)) | ||
Theorem | itgsub 25342* | Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ โซ๐ด(๐ต โ ๐ถ) d๐ฅ = (โซ๐ด๐ต d๐ฅ โ โซ๐ด๐ถ d๐ฅ)) | ||
Theorem | itgfsum 25343* | Take a finite sum of integrals over the same domain. (Contributed by Mario Carneiro, 24-Aug-2014.) |
โข (๐ โ ๐ด โ dom vol) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง (๐ฅ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ ๐) & โข ((๐ โง ๐ โ ๐ต) โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ ((๐ฅ โ ๐ด โฆ ฮฃ๐ โ ๐ต ๐ถ) โ ๐ฟ1 โง โซ๐ดฮฃ๐ โ ๐ต ๐ถ d๐ฅ = ฮฃ๐ โ ๐ต โซ๐ด๐ถ d๐ฅ)) | ||
Theorem | iblabslem 25344* | Lemma for iblabs 25345. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ๐บ = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐นโ๐ต)), 0)) & โข (๐ โ (๐ฅ โ ๐ด โฆ (๐นโ๐ต)) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ (๐นโ๐ต) โ โ) โ โข (๐ โ (๐บ โ MblFn โง (โซ2โ๐บ) โ โ)) | ||
Theorem | iblabs 25345* | The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ (๐ฅ โ ๐ด โฆ (absโ๐ต)) โ ๐ฟ1) | ||
Theorem | iblabsr 25346* | A measurable function is integrable iff its absolute value is integrable. (See iblabs 25345 for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) & โข (๐ โ (๐ฅ โ ๐ด โฆ (absโ๐ต)) โ ๐ฟ1) โ โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) | ||
Theorem | iblmulc2 25347* | Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ ๐ฟ1) | ||
Theorem | itgmulc2lem1 25348* | Lemma for itgmulc2 25350: positive real case. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ๐ต) โ โข (๐ โ (๐ถ ยท โซ๐ด๐ต d๐ฅ) = โซ๐ด(๐ถ ยท ๐ต) d๐ฅ) | ||
Theorem | itgmulc2lem2 25349* | Lemma for itgmulc2 25350: real case. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (๐ถ ยท โซ๐ด๐ต d๐ฅ) = โซ๐ด(๐ถ ยท ๐ต) d๐ฅ) | ||
Theorem | itgmulc2 25350* | Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ (๐ถ ยท โซ๐ด๐ต d๐ฅ) = โซ๐ด(๐ถ ยท ๐ต) d๐ฅ) | ||
Theorem | itgabs 25351* | The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) โ โข (๐ โ (absโโซ๐ด๐ต d๐ฅ) โค โซ๐ด(absโ๐ต) d๐ฅ) | ||
Theorem | itgsplit 25352* | The โซ integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014.) |
โข (๐ โ (vol*โ(๐ด โฉ ๐ต)) = 0) & โข (๐ โ ๐ = (๐ด โช ๐ต)) & โข ((๐ โง ๐ฅ โ ๐) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1) & โข (๐ โ (๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ โซ๐๐ถ d๐ฅ = (โซ๐ด๐ถ d๐ฅ + โซ๐ต๐ถ d๐ฅ)) | ||
Theorem | itgspliticc 25353* | The โซ integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ต โ (๐ด[,]๐ถ)) & โข ((๐ โง ๐ฅ โ (๐ด[,]๐ถ)) โ ๐ท โ ๐) & โข (๐ โ (๐ฅ โ (๐ด[,]๐ต) โฆ ๐ท) โ ๐ฟ1) & โข (๐ โ (๐ฅ โ (๐ต[,]๐ถ) โฆ ๐ท) โ ๐ฟ1) โ โข (๐ โ โซ(๐ด[,]๐ถ)๐ท d๐ฅ = (โซ(๐ด[,]๐ต)๐ท d๐ฅ + โซ(๐ต[,]๐ถ)๐ท d๐ฅ)) | ||
Theorem | itgsplitioo 25354* | The โซ integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ต โ (๐ด[,]๐ถ)) & โข ((๐ โง ๐ฅ โ (๐ด(,)๐ถ)) โ ๐ท โ โ) & โข (๐ โ (๐ฅ โ (๐ด(,)๐ต) โฆ ๐ท) โ ๐ฟ1) & โข (๐ โ (๐ฅ โ (๐ต(,)๐ถ) โฆ ๐ท) โ ๐ฟ1) โ โข (๐ โ โซ(๐ด(,)๐ถ)๐ท d๐ฅ = (โซ(๐ด(,)๐ต)๐ท d๐ฅ + โซ(๐ต(,)๐ถ)๐ท d๐ฅ)) | ||
Theorem | bddmulibl 25355* | A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
โข ((๐น โ MblFn โง ๐บ โ ๐ฟ1 โง โ๐ฅ โ โ โ๐ฆ โ dom ๐น(absโ(๐นโ๐ฆ)) โค ๐ฅ) โ (๐น โf ยท ๐บ) โ ๐ฟ1) | ||
Theorem | bddibl 25356* | A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
โข ((๐น โ MblFn โง (volโdom ๐น) โ โ โง โ๐ฅ โ โ โ๐ฆ โ dom ๐น(absโ(๐นโ๐ฆ)) โค ๐ฅ) โ ๐น โ ๐ฟ1) | ||
Theorem | cniccibl 25357 | A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐น โ ((๐ด[,]๐ต)โcnโโ)) โ ๐น โ ๐ฟ1) | ||
Theorem | bddiblnc 25358* | Choice-free proof of bddibl 25356. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.) |
โข ((๐น โ MblFn โง (volโdom ๐น) โ โ โง โ๐ฅ โ โ โ๐ฆ โ dom ๐น(absโ(๐นโ๐ฆ)) โค ๐ฅ) โ ๐น โ ๐ฟ1) | ||
Theorem | cnicciblnc 25359 | Choice-free proof of cniccibl 25357. (Contributed by Brendan Leahy, 2-Nov-2017.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐น โ ((๐ด[,]๐ต)โcnโโ)) โ ๐น โ ๐ฟ1) | ||
Theorem | itggt0 25360* | The integral of a strictly positive function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.) |
โข (๐ โ 0 < (volโ๐ด)) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ+) โ โข (๐ โ 0 < โซ๐ด๐ต d๐ฅ) | ||
Theorem | itgcn 25361* | Transfer itg2cn 25280 to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ โ๐ โ โ+ โ๐ข โ dom vol((๐ข โ ๐ด โง (volโ๐ข) < ๐) โ โซ๐ข(absโ๐ต) d๐ฅ < ๐ถ)) | ||
Syntax | cdit 25362 | Extend class notation with the directed integral. |
class โจ[๐ด โ ๐ต]๐ถ d๐ฅ | ||
Definition | df-ditg 25363 | Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The ๐ด and ๐ต here are the lower and upper limits of the integral, usually written as a subscript and superscript next to the integral sign. We define the region of integration to be an open interval instead of closed so that we can use +โ, -โ for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข โจ[๐ด โ ๐ต]๐ถ d๐ฅ = if(๐ด โค ๐ต, โซ(๐ด(,)๐ต)๐ถ d๐ฅ, -โซ(๐ต(,)๐ด)๐ถ d๐ฅ) | ||
Theorem | ditgeq1 25364* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ด = ๐ต โ โจ[๐ด โ ๐ถ]๐ท d๐ฅ = โจ[๐ต โ ๐ถ]๐ท d๐ฅ) | ||
Theorem | ditgeq2 25365* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ด = ๐ต โ โจ[๐ถ โ ๐ด]๐ท d๐ฅ = โจ[๐ถ โ ๐ต]๐ท d๐ฅ) | ||
Theorem | ditgeq3 25366* | Equality theorem for the directed integral. (The domain of the equality here is very rough; for more precise bounds one should decompose it with ditgpos 25372 first and use the equality theorems for df-itg 25139.) (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (โ๐ฅ โ โ ๐ท = ๐ธ โ โจ[๐ด โ ๐ต]๐ท d๐ฅ = โจ[๐ด โ ๐ต]๐ธ d๐ฅ) | ||
Theorem | ditgeq3dv 25367* | Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข ((๐ โง ๐ฅ โ โ) โ ๐ท = ๐ธ) โ โข (๐ โ โจ[๐ด โ ๐ต]๐ท d๐ฅ = โจ[๐ด โ ๐ต]๐ธ d๐ฅ) | ||
Theorem | ditgex 25368 | A directed integral is a set. (Contributed by Mario Carneiro, 7-Sep-2014.) |
โข โจ[๐ด โ ๐ต]๐ถ d๐ฅ โ V | ||
Theorem | ditg0 25369* | Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข โจ[๐ด โ ๐ด]๐ต d๐ฅ = 0 | ||
Theorem | cbvditg 25370* | Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.) |
โข (๐ฅ = ๐ฆ โ ๐ถ = ๐ท) & โข โฒ๐ฆ๐ถ & โข โฒ๐ฅ๐ท โ โข โจ[๐ด โ ๐ต]๐ถ d๐ฅ = โจ[๐ด โ ๐ต]๐ท d๐ฆ | ||
Theorem | cbvditgv 25371* | Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.) |
โข (๐ฅ = ๐ฆ โ ๐ถ = ๐ท) โ โข โจ[๐ด โ ๐ต]๐ถ d๐ฅ = โจ[๐ด โ ๐ต]๐ท d๐ฆ | ||
Theorem | ditgpos 25372* | Value of the directed integral in the forward direction. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ โ ๐ด โค ๐ต) โ โข (๐ โ โจ[๐ด โ ๐ต]๐ถ d๐ฅ = โซ(๐ด(,)๐ต)๐ถ d๐ฅ) | ||
Theorem | ditgneg 25373* | Value of the directed integral in the backward direction. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ โจ[๐ต โ ๐ด]๐ถ d๐ฅ = -โซ(๐ด(,)๐ต)๐ถ d๐ฅ) | ||
Theorem | ditgcl 25374* | Closure of a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ (๐[,]๐)) & โข (๐ โ ๐ต โ (๐[,]๐)) & โข ((๐ โง ๐ฅ โ (๐(,)๐)) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ (๐(,)๐) โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ โจ[๐ด โ ๐ต]๐ถ d๐ฅ โ โ) | ||
Theorem | ditgswap 25375* | Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ (๐[,]๐)) & โข (๐ โ ๐ต โ (๐[,]๐)) & โข ((๐ โง ๐ฅ โ (๐(,)๐)) โ ๐ถ โ ๐) & โข (๐ โ (๐ฅ โ (๐(,)๐) โฆ ๐ถ) โ ๐ฟ1) โ โข (๐ โ โจ[๐ต โ ๐ด]๐ถ d๐ฅ = -โจ[๐ด โ ๐ต]๐ถ d๐ฅ) | ||
Theorem | ditgsplitlem 25376* | Lemma for ditgsplit 25377. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ (๐[,]๐)) & โข (๐ โ ๐ต โ (๐[,]๐)) & โข (๐ โ ๐ถ โ (๐[,]๐)) & โข ((๐ โง ๐ฅ โ (๐(,)๐)) โ ๐ท โ ๐) & โข (๐ โ (๐ฅ โ (๐(,)๐) โฆ ๐ท) โ ๐ฟ1) & โข ((๐ โง ๐) โ (๐ด โค ๐ต โง ๐ต โค ๐ถ)) โ โข (((๐ โง ๐) โง ๐) โ โจ[๐ด โ ๐ถ]๐ท d๐ฅ = (โจ[๐ด โ ๐ต]๐ท d๐ฅ + โจ[๐ต โ ๐ถ]๐ท d๐ฅ)) | ||
Theorem | ditgsplit 25377* | This theorem is the raison d'รชtre for the directed integral, because unlike itgspliticc 25353, there is no constraint on the ordering of the points ๐ด, ๐ต, ๐ถ in the domain. (Contributed by Mario Carneiro, 13-Aug-2014.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ (๐[,]๐)) & โข (๐ โ ๐ต โ (๐[,]๐)) & โข (๐ โ ๐ถ โ (๐[,]๐)) & โข ((๐ โง ๐ฅ โ (๐(,)๐)) โ ๐ท โ ๐) & โข (๐ โ (๐ฅ โ (๐(,)๐) โฆ ๐ท) โ ๐ฟ1) โ โข (๐ โ โจ[๐ด โ ๐ถ]๐ท d๐ฅ = (โจ[๐ด โ ๐ต]๐ท d๐ฅ + โจ[๐ต โ ๐ถ]๐ท d๐ฅ)) | ||
Syntax | climc 25378 | The limit operator. |
class limโ | ||
Syntax | cdv 25379 | The derivative operator. |
class D | ||
Syntax | cdvn 25380 | The ๐-th derivative operator. |
class D๐ | ||
Syntax | ccpn 25381 | The set of ๐-times continuously differentiable functions. |
class ๐C๐ | ||
Definition | df-limc 25382* | Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.) |
โข limโ = (๐ โ (โ โpm โ), ๐ฅ โ โ โฆ {๐ฆ โฃ [(TopOpenโโfld) / ๐](๐ง โ (dom ๐ โช {๐ฅ}) โฆ if(๐ง = ๐ฅ, ๐ฆ, (๐โ๐ง))) โ (((๐ โพt (dom ๐ โช {๐ฅ})) CnP ๐)โ๐ฅ)}) | ||
Definition | df-dv 25383* | Define the derivative operator. This acts on functions to produce a function that is defined where the original function is differentiable, with value the derivative of the function at these points. The set ๐ here is the ambient topological space under which we are evaluating the continuity of the difference quotient. Although the definition is valid for any subset of โ and is well-behaved when ๐ contains no isolated points, we will restrict our attention to the cases ๐ = โ or ๐ = โ for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.) |
โข D = (๐ โ ๐ซ โ, ๐ โ (โ โpm ๐ ) โฆ โช ๐ฅ โ ((intโ((TopOpenโโfld) โพt ๐ ))โdom ๐)({๐ฅ} ร ((๐ง โ (dom ๐ โ {๐ฅ}) โฆ (((๐โ๐ง) โ (๐โ๐ฅ)) / (๐ง โ ๐ฅ))) limโ ๐ฅ))) | ||
Definition | df-dvn 25384* | Define the ๐-th derivative operator on functions on the complex numbers. This just iterates the derivative operation according to the last argument. (Contributed by Mario Carneiro, 11-Feb-2015.) |
โข D๐ = (๐ โ ๐ซ โ, ๐ โ (โ โpm ๐ ) โฆ seq0(((๐ฅ โ V โฆ (๐ D ๐ฅ)) โ 1st ), (โ0 ร {๐}))) | ||
Definition | df-cpn 25385* | Define the set of ๐-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
โข ๐C๐ = (๐ โ ๐ซ โ โฆ (๐ฅ โ โ0 โฆ {๐ โ (โ โpm ๐ ) โฃ ((๐ D๐ ๐)โ๐ฅ) โ (dom ๐โcnโโ)})) | ||
Theorem | reldv 25386 | The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 24-Dec-2016.) |
โข Rel (๐ D ๐น) | ||
Theorem | limcvallem 25387* | Lemma for ellimc 25389. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข ๐ฝ = (๐พ โพt (๐ด โช {๐ต})) & โข ๐พ = (TopOpenโโfld) & โข ๐บ = (๐ง โ (๐ด โช {๐ต}) โฆ if(๐ง = ๐ต, ๐ถ, (๐นโ๐ง))) โ โข ((๐น:๐ดโถโ โง ๐ด โ โ โง ๐ต โ โ) โ (๐บ โ ((๐ฝ CnP ๐พ)โ๐ต) โ ๐ถ โ โ)) | ||
Theorem | limcfval 25388* | Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข ๐ฝ = (๐พ โพt (๐ด โช {๐ต})) & โข ๐พ = (TopOpenโโfld) โ โข ((๐น:๐ดโถโ โง ๐ด โ โ โง ๐ต โ โ) โ ((๐น limโ ๐ต) = {๐ฆ โฃ (๐ง โ (๐ด โช {๐ต}) โฆ if(๐ง = ๐ต, ๐ฆ, (๐นโ๐ง))) โ ((๐ฝ CnP ๐พ)โ๐ต)} โง (๐น limโ ๐ต) โ โ)) | ||
Theorem | ellimc 25389* | Value of the limit predicate. ๐ถ is the limit of the function ๐น at ๐ต if the function ๐บ, formed by adding ๐ต to the domain of ๐น and setting it to ๐ถ, is continuous at ๐ต. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข ๐ฝ = (๐พ โพt (๐ด โช {๐ต})) & โข ๐พ = (TopOpenโโfld) & โข ๐บ = (๐ง โ (๐ด โช {๐ต}) โฆ if(๐ง = ๐ต, ๐ถ, (๐นโ๐ง))) & โข (๐ โ ๐น:๐ดโถโ) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ถ โ (๐น limโ ๐ต) โ ๐บ โ ((๐ฝ CnP ๐พ)โ๐ต))) | ||
Theorem | limcrcl 25390 | Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.) |
โข (๐ถ โ (๐น limโ ๐ต) โ (๐น:dom ๐นโถโ โง dom ๐น โ โ โง ๐ต โ โ)) | ||
Theorem | limccl 25391 | Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐น limโ ๐ต) โ โ | ||
Theorem | limcdif 25392 | It suffices to consider functions which are not defined at ๐ต to define the limit of a function. In particular, the value of the original function ๐น at ๐ต does not affect the limit of ๐น. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐ โ ๐น:๐ดโถโ) โ โข (๐ โ (๐น limโ ๐ต) = ((๐น โพ (๐ด โ {๐ต})) limโ ๐ต)) | ||
Theorem | ellimc2 25393* | Write the definition of a limit directly in terms of open sets of the topology on the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐ โ ๐น:๐ดโถโ) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข ๐พ = (TopOpenโโfld) โ โข (๐ โ (๐ถ โ (๐น limโ ๐ต) โ (๐ถ โ โ โง โ๐ข โ ๐พ (๐ถ โ ๐ข โ โ๐ค โ ๐พ (๐ต โ ๐ค โง (๐น โ (๐ค โฉ (๐ด โ {๐ต}))) โ ๐ข))))) | ||
Theorem | limcnlp 25394 | If ๐ต is not a limit point of the domain of the function ๐น, then every point is a limit of ๐น at ๐ต. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐ โ ๐น:๐ดโถโ) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข ๐พ = (TopOpenโโfld) & โข (๐ โ ยฌ ๐ต โ ((limPtโ๐พ)โ๐ด)) โ โข (๐ โ (๐น limโ ๐ต) = โ) | ||
Theorem | ellimc3 25395* | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) |
โข (๐ โ ๐น:๐ดโถโ) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ถ โ (๐น limโ ๐ต) โ (๐ถ โ โ โง โ๐ฅ โ โ+ โ๐ฆ โ โ+ โ๐ง โ ๐ด ((๐ง โ ๐ต โง (absโ(๐ง โ ๐ต)) < ๐ฆ) โ (absโ((๐นโ๐ง) โ ๐ถ)) < ๐ฅ)))) | ||
Theorem | limcflflem 25396 | Lemma for limcflf 25397. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐ โ ๐น:๐ดโถโ) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ ((limPtโ๐พ)โ๐ด)) & โข ๐พ = (TopOpenโโfld) & โข ๐ถ = (๐ด โ {๐ต}) & โข ๐ฟ = (((neiโ๐พ)โ{๐ต}) โพt ๐ถ) โ โข (๐ โ ๐ฟ โ (Filโ๐ถ)) | ||
Theorem | limcflf 25397 | The limit operator can be expressed as a filter limit, from the filter of neighborhoods of ๐ต restricted to ๐ด โ {๐ต}, to the topology of the complex numbers. (If ๐ต is not a limit point of ๐ด, then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐ โ ๐น:๐ดโถโ) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ ((limPtโ๐พ)โ๐ด)) & โข ๐พ = (TopOpenโโfld) & โข ๐ถ = (๐ด โ {๐ต}) & โข ๐ฟ = (((neiโ๐พ)โ{๐ต}) โพt ๐ถ) โ โข (๐ โ (๐น limโ ๐ต) = ((๐พ fLimf ๐ฟ)โ(๐น โพ ๐ถ))) | ||
Theorem | limcmo 25398* | If ๐ต is a limit point of the domain of the function ๐น, then there is at most one limit value of ๐น at ๐ต. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐ โ ๐น:๐ดโถโ) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ ((limPtโ๐พ)โ๐ด)) & โข ๐พ = (TopOpenโโfld) โ โข (๐ โ โ*๐ฅ ๐ฅ โ (๐น limโ ๐ต)) | ||
Theorem | limcmpt 25399* | Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข ((๐ โง ๐ง โ ๐ด) โ ๐ท โ โ) & โข ๐ฝ = (๐พ โพt (๐ด โช {๐ต})) & โข ๐พ = (TopOpenโโfld) โ โข (๐ โ (๐ถ โ ((๐ง โ ๐ด โฆ ๐ท) limโ ๐ต) โ (๐ง โ (๐ด โช {๐ต}) โฆ if(๐ง = ๐ต, ๐ถ, ๐ท)) โ ((๐ฝ CnP ๐พ)โ๐ต))) | ||
Theorem | limcmpt2 25400* | Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ ๐ด) & โข ((๐ โง (๐ง โ ๐ด โง ๐ง โ ๐ต)) โ ๐ท โ โ) & โข ๐ฝ = (๐พ โพt ๐ด) & โข ๐พ = (TopOpenโโfld) โ โข (๐ โ (๐ถ โ ((๐ง โ (๐ด โ {๐ต}) โฆ ๐ท) limโ ๐ต) โ (๐ง โ ๐ด โฆ if(๐ง = ๐ต, ๐ถ, ๐ท)) โ ((๐ฝ CnP ๐พ)โ๐ต))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |