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

Definition df-mbf 23433
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 23340) 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 23428 . 2 class MblFn
2 cre 13881 . . . . . . . . 9 class
3 vf . . . . . . . . . 10 setvar 𝑓
43cv 1522 . . . . . . . . 9 class 𝑓
52, 4ccom 5147 . . . . . . . 8 class (ℜ ∘ 𝑓)
65ccnv 5142 . . . . . . 7 class (ℜ ∘ 𝑓)
7 vx . . . . . . . 8 setvar 𝑥
87cv 1522 . . . . . . 7 class 𝑥
96, 8cima 5146 . . . . . 6 class ((ℜ ∘ 𝑓) “ 𝑥)
10 cvol 23278 . . . . . . 7 class vol
1110cdm 5143 . . . . . 6 class dom vol
129, 11wcel 2030 . . . . 5 wff ((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol
13 cim 13882 . . . . . . . . 9 class
1413, 4ccom 5147 . . . . . . . 8 class (ℑ ∘ 𝑓)
1514ccnv 5142 . . . . . . 7 class (ℑ ∘ 𝑓)
1615, 8cima 5146 . . . . . 6 class ((ℑ ∘ 𝑓) “ 𝑥)
1716, 11wcel 2030 . . . . 5 wff ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol
1812, 17wa 383 . . . 4 wff (((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
19 cioo 12213 . . . . 5 class (,)
2019crn 5144 . . . 4 class ran (,)
2118, 7, 20wral 2941 . . 3 wff 𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
22 cc 9972 . . . 4 class
23 cr 9973 . . . 4 class
24 cpm 7900 . . . 4 class pm
2522, 23, 24co 6690 . . 3 class (ℂ ↑pm ℝ)
2621, 3, 25crab 2945 . 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
271, 26wceq 1523 1 wff MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
Colors of variables: wff setvar class
This definition is referenced by:  ismbf1  23438
  Copyright terms: Public domain W3C validator