Description: A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | mbff | |- ( F e. MblFn -> F : dom F --> CC ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismbf1 | |- ( F e. MblFn <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) ) |
|
2 | 1 | simplbi | |- ( F e. MblFn -> F e. ( CC ^pm RR ) ) |
3 | cnex | |- CC e. _V |
|
4 | reex | |- RR e. _V |
|
5 | 3 4 | elpm2 | |- ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) ) |
6 | 5 | simplbi | |- ( F e. ( CC ^pm RR ) -> F : dom F --> CC ) |
7 | 2 6 | syl | |- ( F e. MblFn -> F : dom F --> CC ) |