Description: Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | i1fmbf | |- ( F e. dom S.1 -> F e. MblFn ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isi1f | |- ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) ) |
|
2 | 1 | simplbi | |- ( F e. dom S.1 -> F e. MblFn ) |