Positive real step function
Set
| context | ⟨X,Σ⟩∈MeasurableSpace(X) |
| postulate | f∈T+ |
| context | f∈T | context | …Real step function |
| x∈X |
| postulate | f(x)≥0 |
Discussion
Parents
Subset of
| context | ⟨X,Σ⟩∈MeasurableSpace(X) |
| postulate | f∈T+ |
| context | f∈T | context | …Real step function |
| x∈X |
| postulate | f(x)≥0 |
