Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | smflimsup.n | |
|
smflimsup.x | |
||
smflimsup.m | |
||
smflimsup.z | |
||
smflimsup.s | |
||
smflimsup.f | |
||
smflimsup.d | |
||
smflimsup.g | |
||
Assertion | smflimsup | |