Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-oms Structured version   Visualization version   GIF version

Definition df-oms 32259
Description: Define a function constructing an outer measure. See omsval 32260 for its value. Definition 1.5 of [Bogachev] p. 16. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
Assertion
Ref Expression
df-oms toOMeas = (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑟𝑦)), (0[,]+∞), < )))
Distinct variable group:   𝑟,𝑎,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-oms
StepHypRef Expression
1 coms 32258 . 2 class toOMeas
2 vr . . 3 setvar 𝑟
3 cvv 3432 . . 3 class V
4 va . . . 4 setvar 𝑎
52cv 1538 . . . . . . 7 class 𝑟
65cdm 5589 . . . . . 6 class dom 𝑟
76cuni 4839 . . . . 5 class dom 𝑟
87cpw 4533 . . . 4 class 𝒫 dom 𝑟
9 vx . . . . . . 7 setvar 𝑥
104cv 1538 . . . . . . . . . 10 class 𝑎
11 vz . . . . . . . . . . . 12 setvar 𝑧
1211cv 1538 . . . . . . . . . . 11 class 𝑧
1312cuni 4839 . . . . . . . . . 10 class 𝑧
1410, 13wss 3887 . . . . . . . . 9 wff 𝑎 𝑧
15 com 7712 . . . . . . . . . 10 class ω
16 cdom 8731 . . . . . . . . . 10 class
1712, 15, 16wbr 5074 . . . . . . . . 9 wff 𝑧 ≼ ω
1814, 17wa 396 . . . . . . . 8 wff (𝑎 𝑧𝑧 ≼ ω)
196cpw 4533 . . . . . . . 8 class 𝒫 dom 𝑟
2018, 11, 19crab 3068 . . . . . . 7 class {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 𝑧𝑧 ≼ ω)}
219cv 1538 . . . . . . . 8 class 𝑥
22 vy . . . . . . . . . 10 setvar 𝑦
2322cv 1538 . . . . . . . . 9 class 𝑦
2423, 5cfv 6433 . . . . . . . 8 class (𝑟𝑦)
2521, 24, 22cesum 31995 . . . . . . 7 class Σ*𝑦𝑥(𝑟𝑦)
269, 20, 25cmpt 5157 . . . . . 6 class (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑟𝑦))
2726crn 5590 . . . . 5 class ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑟𝑦))
28 cc0 10871 . . . . . 6 class 0
29 cpnf 11006 . . . . . 6 class +∞
30 cicc 13082 . . . . . 6 class [,]
3128, 29, 30co 7275 . . . . 5 class (0[,]+∞)
32 clt 11009 . . . . 5 class <
3327, 31, 32cinf 9200 . . . 4 class inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑟𝑦)), (0[,]+∞), < )
344, 8, 33cmpt 5157 . . 3 class (𝑎 ∈ 𝒫 dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑟𝑦)), (0[,]+∞), < ))
352, 3, 34cmpt 5157 . 2 class (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑟𝑦)), (0[,]+∞), < )))
361, 35wceq 1539 1 wff toOMeas = (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 𝑧𝑧 ≼ ω)} ↦ Σ*𝑦𝑥(𝑟𝑦)), (0[,]+∞), < )))
Colors of variables: wff setvar class
This definition is referenced by:  omsval  32260
  Copyright terms: Public domain W3C validator