Let $(X,\mathcal{A},\mu)$ be a measure space and $f:X\to [0,\infty]$ be a function. Define the integral of $f$ by
$$L(f)=\sup\bigg\{ \sum_{k=1}^n\inf\{f(x):x\in E_k\}\mu(E_k):\{E_k\} \text{ is a finite measurable partition of } X \bigg \}$$
I want to show that this definition is equivalent to the usual one:
$$\int f=\sup\bigg\{\int s:0\leq s\leq f, s \text{ simple } \bigg \}$$
where a simple function is a measurable real function on $X$ taking a finite number of values.
If $s\leq f$ is a nonnegative simple function with standard representation $s=\sum_{k=1}^n \alpha_k\chi_{E_k}$ , then $\alpha_k=\inf\{s(x):x\in E_k\}\leq \inf\{f(x):x\in E_k\} $ $(1\leq k\leq n)$ and $\{E_k\}$ is a finite measurable partition of $X$ so we see that $\int s\leq L(f)$. The function $s$ being arbitrary we conclude that $\int f \leq L(f)$.
Conversely if $\{E_k\}$ is any finite measurable partition of $X$ and we set $\alpha_k:=\inf\{f(x):x\in E_k\}$ $(1\leq k\leq n)$, then $s:=\sum_{k=1}^n \alpha_k\chi_{E_k}$ is a nonnegative function. If each $\alpha_k$ is real then it is also a simple function. More generally, if $\alpha_k =\infty$ for some $k$, then there exist a sequence of nonnegative simple functions $s_n$ increasing to $s$ pointwise on $X$ (replace $\alpha_k$ by $n$ in $s_n$ for each $k$ such that $\alpha_k =\infty$ ). We also check that $\int s_n \uparrow \sum_{k=1}^n\alpha_k\mu(E_k)$. Therefore $\int s \geq \sum_{k=1}^n\alpha_k\mu(E_k)$. Since $s\leq f$ we get $$\int f \geq \int s \geq \sum_{k=1}^n\alpha_k\mu(E_k)$$ Finally since the partition was aribtrary we conclude $\int f \geq L(f)$.
Is this correct?