Real step function
Set
| context | ⟨X,Σ⟩∈MeasurableSpace(X) |
| postulate | f∈T |
| context | f∈Measurable(X,R) |
Where we consider the Borel algebra over R
| postulate | im(f) … finite |
Discussion
These functions can be written as
f=∑nj=1αj⋅χEn
with αj's real numbers and En's in the measurable algebra.
Parents
Refinement of
Context
