Description: The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | smflim.n | |
|
smflim.x | |
||
smflim.m | |
||
smflim.z | |
||
smflim.s | |
||
smflim.f | |
||
smflim.d | |
||
smflim.g | |
||
Assertion | smflim | |