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 24149
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 24056) 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 24144 . 2 class MblFn
2 cre 14446 . . . . . . . . 9 class
3 vf . . . . . . . . . 10 setvar 𝑓
43cv 1527 . . . . . . . . 9 class 𝑓
52, 4ccom 5553 . . . . . . . 8 class (ℜ ∘ 𝑓)
65ccnv 5548 . . . . . . 7 class (ℜ ∘ 𝑓)
7 vx . . . . . . . 8 setvar 𝑥
87cv 1527 . . . . . . 7 class 𝑥
96, 8cima 5552 . . . . . 6 class ((ℜ ∘ 𝑓) “ 𝑥)
10 cvol 23993 . . . . . . 7 class vol
1110cdm 5549 . . . . . 6 class dom vol
129, 11wcel 2105 . . . . 5 wff ((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol
13 cim 14447 . . . . . . . . 9 class
1413, 4ccom 5553 . . . . . . . 8 class (ℑ ∘ 𝑓)
1514ccnv 5548 . . . . . . 7 class (ℑ ∘ 𝑓)
1615, 8cima 5552 . . . . . 6 class ((ℑ ∘ 𝑓) “ 𝑥)
1716, 11wcel 2105 . . . . 5 wff ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol
1812, 17wa 396 . . . 4 wff (((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
19 cioo 12728 . . . . 5 class (,)
2019crn 5550 . . . 4 class ran (,)
2118, 7, 20wral 3138 . . 3 wff 𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)
22 cc 10524 . . . 4 class
23 cr 10525 . . . 4 class
24 cpm 8397 . . . 4 class pm
2522, 23, 24co 7145 . . 3 class (ℂ ↑pm ℝ)
2621, 3, 25crab 3142 . 2 class {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
271, 26wceq 1528 1 wff MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
Colors of variables: wff setvar class
This definition is referenced by:  ismbf1  24154
  Copyright terms: Public domain W3C validator