定理93

定理93を論理式にすると
\[ \begin{align} &\forall\mu,E\ (\mbox{\(\mu\)は測度}\land\mbox{\(E\)はM集合}\land\mu E \ne \infty \to \\ &~~~\forall f,F\ (\mbox{\(f\)はM函数} \land \mbox{\(F\)は加法的集合函数} \to \\ &~~~~~~\forall a,b\ (\mbox{\(a,b\)は実数}\land -\infty \leq a \leq b \leq \infty\ \to \\ &~~~~~~~~~(\forall e\ \mbox{\(e\)はM集合}\land e \subset E\{a\leq f \leq b\} \to (a\mu e \leq F(e) \leq b\mu e)) \tag{17}\\ &~~~~~~) \\ &~~~~~~\to F(E) = \int_E f\,d\mu \tag{B}\\ &~~~) \\ &) \end{align} \] 定理の本体は、(17) ⇒ (B) の部分である。日本語に翻訳すると
"Fが領域の至る所で平均値の性質を満たすならばFは積分に等しい"
となる。定理93はFについての定理である。

"\(\to\)" がネストしてると非常にわかりにくいのでちょっと整理してみると \[ \begin{align} \forall\mu,E,f,F\ \ & \mu E \ne \infty \land (\forall a,b,e\ -\infty \leq a \leq b \leq \infty \land e \subset E\{a\leq f \leq b\} \to a\mu e \leq F(e) \leq b\mu e ) \\ &\to F(E) = \int_E f\,d\mu \\ \end{align} \] となる。ただし \(\mbox{\(\mu\)は測度},\ \mbox{\(E\)はM集合},\cdots\) などは省略した。また \(A\to(B\to C) \equiv A\land B \to C\) (条件部をまとめる) と \(\forall x\ f(x) \land (\forall y\ g(x,y)) \equiv \forall x,y\ f(x) \land g(x,y) \) (量化子を冠頭にまとめる)を使った。\(a,b,e\)はグローバルスコープにもできるが、局所スコープのままのほうがわかりやすい。また、"\(\to\)" のネストが1つ残っているが、\((A\to B)\to C\)という形は"\(\to\)"を1つに簡略化できないので仕方がない。