Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mbf Structured version   Visualization version   GIF version

Definition df-mbf 23194
 Description: Define the class of measurable functions on the reals. A real function is measurable if the preimage of every open interval is a measurable set (see ismbl 23101) and a complex function is measurable if the real and imaginary parts of the function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
Assertion
Ref Expression
df-mbf MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
Distinct variable group:   𝑥,𝑓

Detailed syntax breakdown of Definition df-mbf
StepHypRef Expression
1 cmbf 23189 . 2 class MblFn
2 cre 13685 . . . . . . . . 9 class
3 vf . . . . . . . . . 10 setvar 𝑓
43cv 1474 . . . . . . . . 9 class 𝑓
52, 4ccom 5042 . . . . . . . 8 class (ℜ ∘ 𝑓)
65ccnv 5037 . . . . . . 7 class (ℜ ∘ 𝑓)
7 vx . . . . . . . 8 setvar 𝑥
87cv 1474 . . . . . . 7 class 𝑥
96, 8cima 5041 . . . . . 6 class ((ℜ ∘ 𝑓) “ 𝑥)
10 cvol 23039 . . . . . . 7 class vol
1110cdm 5038 . . . . . 6 class dom vol
129, 11wcel 1977 . . . . 5 wff ((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol
13 cim 13686 . . . . . . . . 9 class
1413, 4ccom 5042 . . . . . . . 8 class (ℑ ∘ 𝑓)
1514ccnv 5037 . . . . . . 7 class (ℑ ∘ 𝑓)
1615, 8cima 5041 . . . . . 6 class ((ℑ ∘ 𝑓) “ 𝑥)
1716, 11wcel 1977 . . . . 5 wff ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol
1812, 17wa 383 . . . 4 wff (((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
19 cioo 12046 . . . . 5 class (,)
2019crn 5039 . . . 4 class ran (,)
2118, 7, 20wral 2896 . . 3 wff 𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
22 cc 9813 . . . 4 class
23 cr 9814 . . . 4 class
24 cpm 7745 . . . 4 class pm
2522, 23, 24co 6549 . . 3 class (ℂ ↑pm ℝ)
2621, 3, 25crab 2900 . 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
271, 26wceq 1475 1 wff MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
 Colors of variables: wff setvar class This definition is referenced by:  ismbf1  23199
 Copyright terms: Public domain W3C validator