Description: The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | smfinfmpt.n | |
|
smfinfmpt.x | |
||
smfinfmpt.y | |
||
smfinfmpt.m | |
||
smfinfmpt.z | |
||
smfinfmpt.s | |
||
smfinfmpt.b | |
||
smfinfmpt.f | |
||
smfinfmpt.d | |
||
smfinfmpt.g | |
||
Assertion | smfinfmpt | |