![]() |
Metamath
Proof Explorer Theorem List (p. 448 of 473) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | psmeasurelem 44701* | 𝑀 applied to a disjoint union of subsets of its domain is the sum of 𝑀 applied to such subset. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞)) & ⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦ (Σ^‘(𝐻 ↾ 𝑥))) & ⊢ (𝜑 → 𝑀:𝒫 𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝑌 𝑦) ⇒ ⊢ (𝜑 → (𝑀‘∪ 𝑌) = (Σ^‘(𝑀 ↾ 𝑌))) | ||
Theorem | psmeasure 44702* | Point supported measure, Remark 112B (d) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞)) & ⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦ (Σ^‘(𝐻 ↾ 𝑥))) ⇒ ⊢ (𝜑 → 𝑀 ∈ Meas) | ||
Theorem | voliunsge0lem 44703* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝑆 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))) & ⊢ (𝜑 → 𝐸:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) ⇒ ⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) | ||
Theorem | voliunsge0 44704* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐸:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) ⇒ ⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛))))) | ||
Theorem | volmea 44705 | The Lebeasgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → vol ∈ Meas) | ||
Theorem | meage0 44706 | If the measure of a measurable set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑀) ⇒ ⊢ (𝜑 → 0 ≤ (𝑀‘𝐴)) | ||
Theorem | meadjunre 44707 | The measure of the union of two disjoint sets, with finite measure, is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ 𝑆 = dom 𝑀 & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ) & ⊢ (𝜑 → (𝑀‘𝐵) ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) + (𝑀‘𝐵))) | ||
Theorem | meassre 44708 | If the measure of a measurable set is real, then the measure of any of its measurable subsets is real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑀) & ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑀) ⇒ ⊢ (𝜑 → (𝑀‘𝐵) ∈ ℝ) | ||
Theorem | meale0eq0 44709 | A measure that is less than or equal to 0 is 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑀) & ⊢ (𝜑 → (𝑀‘𝐴) ≤ 0) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) = 0) | ||
Theorem | meadif 44710 | The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑀) & ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑀‘(𝐴 ∖ 𝐵)) = ((𝑀‘𝐴) − (𝑀‘𝐵))) | ||
Theorem | meaiuninclem 44711* | Measures are continuous from below (bounded case): if 𝐸 is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiuninc 44712* | Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiuninc2 44713* | Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝐵) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiunincf 44714* | Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐸 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiuninc3v 44715* | Measures are continuous from below: if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 44712 and meaiuninc2 44713 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiuninc3 44716* | Measures are continuous from below: if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 44712 and meaiuninc2 44713 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐸 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiininclem 44717* | Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑁)) & ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) & ⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiininc 44718* | Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑁)) & ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Theorem | meaiininc2 44719* | Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ Meas) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) & ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝑀‘(𝐸‘𝑘)) ∈ ℝ) & ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) | ||
Proofs for most of the theorems in section 113 of [Fremlin1] | ||
Syntax | come 44720 | Extend class notation with the class of outer measures. |
class OutMeas | ||
Definition | df-ome 44721* | Define the class of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))))} | ||
Syntax | ccaragen 44722 | Extend class notation with a function that takes an outer measure and generates a sigma-algebra and a measure. |
class CaraGen | ||
Definition | df-caragen 44723* | Define the sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)}) | ||
Theorem | caragenval 44724* | The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑂 ∈ OutMeas → (CaraGen‘𝑂) = {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)}) | ||
Theorem | isome 44725* | Express the predicate "𝑂 is an outer measure." Definition 113A of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^‘(𝑂 ↾ 𝑦)))))) | ||
Theorem | caragenel 44726* | Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → (𝐸 ∈ 𝑆 ↔ (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)))) | ||
Theorem | omef 44727 | An outer measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 ⇒ ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) | ||
Theorem | ome0 44728 | The outer measure of the empty set is 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) ⇒ ⊢ (𝜑 → (𝑂‘∅) = 0) | ||
Theorem | omessle 44729 | The outer measure of a set is greater than or equal to the measure of a subset, Definition 113A (ii) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐵 ⊆ 𝑋) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ≤ (𝑂‘𝐵)) | ||
Theorem | omedm 44730 | The domain of an outer measure is a power set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑂 ∈ OutMeas → dom 𝑂 = 𝒫 ∪ dom 𝑂) | ||
Theorem | caragensplit 44731 | If 𝐸 is in the set generated by the Caratheodory's method, then it splits any set 𝐴 in two parts such that the sum of the outer measures of the two parts is equal to the outer measure of the whole set 𝐴. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸))) = (𝑂‘𝐴)) | ||
Theorem | caragenelss 44732 | An element of the Caratheodory's construction is a subset of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ 𝑋 = ∪ dom 𝑂 ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝑋) | ||
Theorem | carageneld 44733* | Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎)) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑆) | ||
Theorem | omecl 44734 | The outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ∈ (0[,]+∞)) | ||
Theorem | caragenss 44735 | The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the domain of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂) | ||
Theorem | omeunile 44736 | The outer measure of the union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋) & ⊢ (𝜑 → 𝑌 ≼ ω) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^‘(𝑂 ↾ 𝑌))) | ||
Theorem | caragen0 44737 | The empty set belongs to any Caratheodory's construction. First part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑆) | ||
Theorem | omexrcl 44738 | The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ*) | ||
Theorem | caragenunidm 44739 | The base set of an outer measure belongs to the sigma-algebra generated by the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑆) | ||
Theorem | caragensspw 44740 | The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the power set of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝒫 𝑋) | ||
Theorem | omessre 44741 | If the outer measure of a set is real, then the outer measure of any of its subset is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑂‘𝐵) ∈ ℝ) | ||
Theorem | caragenuni 44742 | The base set of the sigma-algebra generated by the Caratheodory's construction is the whole base set of the original outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → ∪ 𝑆 = ∪ dom 𝑂) | ||
Theorem | caragenuncllem 44743 | The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹))) +𝑒 (𝑂‘(𝐴 ∖ (𝐸 ∪ 𝐹)))) = (𝑂‘𝐴)) | ||
Theorem | caragenuncl 44744 | The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | caragendifcl 44745 | The Caratheodory's construction is closed under the complement operation. Second part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | caragenfiiuncl 44746* | The Caratheodory's construction is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | omeunle 44747 | The outer measure of the union of two sets is less than or equal to the sum of the measures, Remark 113B (c) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → 𝐵 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘(𝐴 ∪ 𝐵)) ≤ ((𝑂‘𝐴) +𝑒 (𝑂‘𝐵))) | ||
Theorem | omeiunle 44748* | The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐸 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | omelesplit 44749 | The outer measure of a set 𝐴 is less than or equal to the extended addition of the outer measures of the decomposition induced on 𝐴 by any 𝐸. Step (a) in the proof of Caratheodory's Method, Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ≤ ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸)))) | ||
Theorem | omeiunltfirp 44750* | If the outer measure of a countable union is not +∞, then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋) & ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐸‘𝑛)) + 𝑌)) | ||
Theorem | omeiunlempt 44751* | The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐸 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 𝐸) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘𝐸)))) | ||
Theorem | carageniuncllem1 44752* | The outer measure of 𝐴 ∩ (𝐺‘𝑛) is the sum of the outer measures of 𝐴 ∩ (𝐹‘𝑚). These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾)))) | ||
Theorem | carageniuncllem2 44753* | The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝐴 ∖ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌)) | ||
Theorem | carageniuncl 44754* | The Caratheodory's construction is closed under indexed countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝑆) | ||
Theorem | caragenunicl 44755 | The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝑋 ≼ ω) ⇒ ⊢ (𝜑 → ∪ 𝑋 ∈ 𝑆) | ||
Theorem | caragensal 44756 | Caratheodory's method generates a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | caratheodorylem1 44757* | Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛)) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | caratheodorylem2 44758* | Caratheodory's construction is sigma-additive. Main part of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸:ℕ⟶𝑆) & ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) & ⊢ 𝐺 = (𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛)) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | caratheodory 44759 | Caratheodory's construction of a measure given an outer measure. Proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → (𝑂 ↾ 𝑆) ∈ Meas) | ||
Theorem | 0ome 44760* | The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑂 = (𝑥 ∈ 𝒫 𝑋 ↦ 0) ⇒ ⊢ (𝜑 → 𝑂 ∈ OutMeas) | ||
Theorem | isomenndlem 44761* | 𝑂 is sub-additive w.r.t. countable indexed union, implies that 𝑂 is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑂‘∅) = 0) & ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) & ⊢ (𝜑 → 𝐵 ⊆ ℕ) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌) & ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^‘(𝑂 ↾ 𝑌))) | ||
Theorem | isomennd 44762* | Sufficient condition to prove that 𝑂 is an outer measure. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑂‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥) → (𝑂‘𝑦) ≤ (𝑂‘𝑥)) & ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ⇒ ⊢ (𝜑 → 𝑂 ∈ OutMeas) | ||
Theorem | caragenel2d 44763* | Membership in the Caratheodory's construction. Similar to carageneld 44733, but here "less then or equal to" is used, instead of equality. This is Remark 113D of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) ≤ (𝑂‘𝑎)) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑆) | ||
Theorem | omege0 44764 | If the outer measure of a set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → 0 ≤ (𝑂‘𝐴)) | ||
Theorem | omess0 44765 | If the outer measure of a set is 0, then the outer measure of its subsets is 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) = 0) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑂‘𝐵) = 0) | ||
Theorem | caragencmpl 44766 | A measure built with the Caratheodory's construction is complete. See Definition 112Df of [Fremlin1] p. 19. This is Exercise 113Xa of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐸 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐸) = 0) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑆) | ||
Proofs for most of the theorems in section 115 of [Fremlin1] | ||
Syntax | covoln 44767 | Extend class notation with the class of Lebesgue outer measure for the space of multidimensional real numbers. |
class voln* | ||
Definition | df-ovoln 44768* | Define the outer measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ voln* = (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )))) | ||
Syntax | cvoln 44769 | Extend class notation with the class of Lebesgue measure for the space of multidimensional real numbers. |
class voln | ||
Definition | df-voln 44770 | Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))) | ||
Theorem | vonval 44771 | Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln‘𝑋) = ((voln*‘𝑋) ↾ (CaraGen‘(voln*‘𝑋)))) | ||
Theorem | ovnval 44772* | Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln*‘𝑋) = (𝑦 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )))) | ||
Theorem | elhoi 44773* | Membership in a multidimensional half-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑌 ∈ ((𝐴[,)𝐵) ↑m 𝑋) ↔ (𝑌:𝑋⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 (𝑌‘𝑥) ∈ (𝐴[,)𝐵)))) | ||
Theorem | icoresmbl 44774 | A closed-below, open-above real interval is measurable, when the bounds are real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ran ([,) ↾ (ℝ × ℝ)) ⊆ dom vol | ||
Theorem | hoissre 44775* | The projection of a half-open interval onto a single dimension is a subset of ℝ. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ 𝐼)‘𝑘) ⊆ ℝ) | ||
Theorem | ovnval2 44776* | Value of the Lebesgue outer measure of a subset 𝐴 of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < ))) | ||
Theorem | volicorecl 44777 | The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ) | ||
Theorem | hoiprodcl 44778* | The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝐼)‘𝑘)) ∈ (0[,)+∞)) | ||
Theorem | hoicvr 44779* | 𝐼 is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) & ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (ℝ ↑m 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) | ||
Theorem | hoissrrn 44780* | A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 (([,) ∘ 𝐼)‘𝑘) ⊆ (ℝ ↑m 𝑋)) | ||
Theorem | ovn0val 44781 | The Lebesgue outer measure (for the zero dimensional space of reals) of every subset is zero. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m ∅)) ⇒ ⊢ (𝜑 → ((voln*‘∅)‘𝐴) = 0) | ||
Theorem | ovnn0val 44782* | The value of a (multidimensional) Lebesgue outer measure, defined on a nonzero-dimensional space of reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | ovnval2b 44783* | Value of the Lebesgue outer measure of a subset 𝐴 of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝐿 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf((𝐿‘𝐴), ℝ*, < ))) | ||
Theorem | volicorescl 44784 | The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝐴 ∈ ran ([,) ↾ (ℝ × ℝ)) → (vol‘𝐴) ∈ ℝ) | ||
Theorem | ovnprodcl 44785* | The product used in the definition of the outer Lebesgue measure in R^n is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐹:ℕ⟶((ℝ × ℝ) ↑m 𝑋)) & ⊢ (𝜑 → 𝐼 ∈ ℕ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐹‘𝐼))‘𝑘)) ∈ (0[,)+∞)) | ||
Theorem | hoiprodcl2 44786* | The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘))) & ⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ (𝜑 → (𝐿‘𝐼) ∈ (0[,)+∞)) | ||
Theorem | hoicvrrex 44787* | Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑌 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | ||
Theorem | ovnsupge0 44788* | The set used in the definition of the Lebesgue outer measure is a subset of the nonnegative extended reals. This is a substep for (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → 𝑀 ⊆ (0[,]+∞)) | ||
Theorem | ovnlecvr 44789* | Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. The statement would also be true with 𝑋 the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘))) & ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑m 𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))))) | ||
Theorem | ovnpnfelsup 44790* | +∞ is an element of the set used in the definition of the Lebesgue outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → +∞ ∈ 𝑀) | ||
Theorem | ovnsslelem 44791* | The (multidimensional, nonzero-dimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} & ⊢ 𝑁 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐵 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ ((voln*‘𝑋)‘𝐵)) | ||
Theorem | ovnssle 44792 | The (multidimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ ((voln*‘𝑋)‘𝐵)) | ||
Theorem | ovnlerp 44793* | The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑀 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) | ||
Theorem | ovnf 44794 | The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln*‘𝑋):𝒫 (ℝ ↑m 𝑋)⟶(0[,]+∞)) | ||
Theorem | ovncvrrp 44795* | The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) & ⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) & ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) ⇒ ⊢ (𝜑 → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸)) | ||
Theorem | ovn0lem 44796* | For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (a)(ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))} & ⊢ (𝜑 → inf(𝑀, ℝ*, < ) ∈ (0[,]+∞)) & ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈1, 0〉)) ⇒ ⊢ (𝜑 → inf(𝑀, ℝ*, < ) = 0) | ||
Theorem | ovn0 44797 | For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘∅) = 0) | ||
Theorem | ovncl 44798 | The Lebesgue outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ (0[,]+∞)) | ||
Theorem | ovn02 44799 | For the zero-dimensional space, voln* assigns zero to every subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (voln*‘∅) = (𝑥 ∈ 𝒫 {∅} ↦ 0) | ||
Theorem | ovnxrcl 44800 | The Lebesgue outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ*) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |