概収束
任意の測度空間$ (X,\mathcal M,\mu)と$ \forall E\in\mathcal M\forall f:E\to\overline\R\forall f_n:\N\to(E\to\overline\R)にて、
$ f_n\to f\quad(n\to\infty)\quad\mu\text{-a.e. on }E
$ :\iff\exist N\in\mu^\gets(\{0\})\forall x\in E\setminus N:f_n(x)\to f(x)\quad(n\to\infty)
を概収束と定義する
https://shosonoda.github.io/lean-ksk2026/blueprint/ch07-measurable-funcs/section-008/#ch07-measurable-funcs-section-008
#2026-07-23 08:09:06