Theorem iblmbf

Description: An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014)

	Ref	Expression
Assertion	iblmbf	$$⊢F\in {𝐿}^1\to F\in MblFn$$

Proof

Step	Hyp	Ref	Expression
1		df-ibl	$$⊢{𝐿}^1=\left\{f\in MblFn|\forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼⦋\Re \left(\frac{f\left(x\right)}{{\mathrm{i}}^k}\right)/y⦌if\left(\left(x\in \mathrm{dom}f\wedge 0\le y\right),y,0\right)\right)\right)\in ℝ\right\}$$
2	1	ssrab3	$$⊢{𝐿}^1\subseteq MblFn$$
3	2	sseli	$$⊢F\in {𝐿}^1\to F\in MblFn$$