![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iblmbf | Structured version Visualization version GIF version |
Description: An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.) |
Ref | Expression |
---|---|
iblmbf | ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ibl 25595 | . . 3 ⊢ 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ} | |
2 | 1 | ssrab3 4076 | . 2 ⊢ 𝐿1 ⊆ MblFn |
3 | 2 | sseli 3972 | 1 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 ∀wral 3050 ⦋csb 3889 ifcif 4530 class class class wbr 5149 ↦ cmpt 5232 dom cdm 5678 ‘cfv 6549 (class class class)co 7419 ℝcr 11139 0cc0 11140 ici 11142 ≤ cle 11281 / cdiv 11903 3c3 12301 ...cfz 13519 ↑cexp 14062 ℜcre 15080 MblFncmbf 25587 ∫2citg2 25589 𝐿1cibl 25590 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-ss 3961 df-ibl 25595 |
This theorem is referenced by: iblcnlem 25762 itgcnlem 25763 itgcnval 25773 itgre 25774 itgim 25775 iblneg 25776 itgneg 25777 iblss 25778 iblss2 25779 itgge0 25784 itgss3 25788 itgless 25790 iblsub 25795 itgadd 25798 itgsub 25799 itgfsum 25800 iblabs 25802 iblmulc2 25804 itgmulc2 25807 itgabs 25808 itgsplit 25809 bddmulibl 25812 itggt0 25817 itgcn 25818 ditgswap 25832 ditgsplitlem 25833 ftc1a 26016 itgsubstlem 26027 iblulm 26388 itgulm 26389 ibladdnc 37281 itgaddnclem1 37282 itgaddnclem2 37283 itgaddnc 37284 iblsubnc 37285 itgsubnc 37286 iblabsnclem 37287 iblabsnc 37288 iblmulc2nc 37289 itgmulc2nclem2 37291 itgmulc2nc 37292 itgabsnc 37293 ftc1cnnclem 37295 ftc1anclem2 37298 ftc1anclem4 37300 ftc1anclem5 37301 ftc1anclem6 37302 ftc1anclem8 37304 |
Copyright terms: Public domain | W3C validator |