P. 247 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24601-24700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	minveclem3b 24601*	Lemma for minvec 24609. The set of vectors within a fixed distance of the infimum forms a filter base. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    ⇒   ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
Theorem	minveclem3 24602*	Lemma for minvec 24609. The filter formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    ⇒   ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))
Theorem	minveclem4a 24603*	Lemma for minvec 24609. 𝐹 converges to a point 𝑃 in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    ⇒   ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
Theorem	minveclem4b 24604*	Lemma for minvec 24609. The convergent point of the Cauchy sequence 𝐹 is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑋)
Theorem	minveclem4 24605*	Lemma for minvec 24609. The convergent point of the Cauchy sequence 𝐹 attains the minimum distance, and so is closer to 𝐴 than any other point in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    &   ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minveclem5 24606*	Lemma for minvec 24609. Discharge the assumptions in minveclem4 24605. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minveclem6 24607*	Lemma for minvec 24609. Any minimal point is less than 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))))
Theorem	minveclem7 24608*	Lemma for minvec 24609. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minvec 24609*	Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace 𝑊 that minimizes the distance to an arbitrary vector 𝐴 in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
12.5.10  Projection Theorem
Theorem	pjthlem1 24610*	Lemma for pjth 24612. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 17-Oct-2015.) (Proof shortened by AV, 10-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂHil)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑁‘𝐴) ≤ (𝑁‘(𝐴 − 𝑥)))    &   ⊢ 𝑇 = ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))    ⇒   ⊢ (𝜑 → (𝐴 , 𝐵) = 0)
Theorem	pjthlem2 24611	Lemma for pjth 24612. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂHil)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑂 = (ocv‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))
Theorem	pjth 24612	Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed uniquely into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑂 = (ocv‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑈 ⊕ (𝑂‘𝑈)) = 𝑉)
Theorem	pjth2 24613	Projection Theorem with abbreviations: A topologically closed subspace is a projection subspace. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐾 = (proj‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ∈ dom 𝐾)
Theorem	cldcss 24614	Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂHil → (𝑈 ∈ 𝐶 ↔ (𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽))))
Theorem	cldcss2 24615	Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂHil → 𝐶 = (𝐿 ∩ (Clsd‘𝐽)))
Theorem	hlhil 24616	Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ Hil)
PART 13  BASIC REAL AND COMPLEX ANALYSIS
13.1  Continuity
Theorem	addcncf 24617*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	subcncf 24618*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	mulcncf 24619*	The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	divcncf 24620*	The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→(ℂ ∖ {0})))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵)) ∈ (𝑋–cn→ℂ))
13.1.1  Intermediate value theorem
Theorem	pmltpclem1 24621*	Lemma for pmltpc 24623. (Contributed by Mario Carneiro, 1-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    &   ⊢ (𝜑 → (((𝐹‘𝐴) < (𝐹‘𝐵) ∧ (𝐹‘𝐶) < (𝐹‘𝐵)) ∨ ((𝐹‘𝐵) < (𝐹‘𝐴) ∧ (𝐹‘𝐵) < (𝐹‘𝐶))))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐)))))
Theorem	pmltpclem2 24622*	Lemma for pmltpc 24623. (Contributed by Mario Carneiro, 1-Jul-2014.)
⊢ (𝜑 → 𝐹 ∈ (ℝ ↑pm ℝ))    &   ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑈 ≤ 𝑉)    &   ⊢ (𝜑 → 𝑊 ≤ 𝑋)    &   ⊢ (𝜑 → ¬ (𝐹‘𝑈) ≤ (𝐹‘𝑉))    &   ⊢ (𝜑 → ¬ (𝐹‘𝑋) ≤ (𝐹‘𝑊))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐)))))
Theorem	pmltpc 24623*	Any function on the reals is either increasing, decreasing, or has a triple of points in a vee formation. (This theorem was created on demand by Mario Carneiro for the 6PCM conference in Bialystok, 1-Jul-2014.) (Contributed by Mario Carneiro, 1-Jul-2014.)
⊢ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)) ∨ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ∨ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))))
Theorem	ivthlem1 24624*	Lemma for ivth 24627. The set 𝑆 of all 𝑥 values with (𝐹‘𝑥) less than 𝑈 is lower bounded by 𝐴 and upper bounded by 𝐵. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵))
Theorem	ivthlem2 24625*	Lemma for ivth 24627. Show that the supremum of 𝑆 cannot be less than 𝑈. If it was, continuity of 𝐹 implies that there are points just above the supremum that are also less than 𝑈, a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}    &   ⊢ 𝐶 = sup(𝑆, ℝ, < )    ⇒   ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈)
Theorem	ivthlem3 24626*	Lemma for ivth 24627, the intermediate value theorem. Show that (𝐹‘𝐶) cannot be greater than 𝑈, and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 17-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈}    &   ⊢ 𝐶 = sup(𝑆, ℝ, < )    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ∧ (𝐹‘𝐶) = 𝑈))
Theorem	ivth 24627*	The intermediate value theorem, increasing case. This is Metamath 100 proof #79. (Contributed by Paul Chapman, 22-Jan-2008.) (Proof shortened by Mario Carneiro, 30-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivth2 24628*	The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthle 24629*	The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐴) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐵)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthle2 24630*	The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    &   ⊢ (𝜑 → ((𝐹‘𝐵) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐴)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈)
Theorem	ivthicc 24631*	The interval between any two points of a continuous real function is contained in the range of the function. Equivalently, the range of a continuous real function is convex. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝑁 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ran 𝐹)
Theorem	evthicc 24632*	Specialization of the Extreme Value Theorem to a closed interval of ℝ. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑥) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(𝐹‘𝑧) ≤ (𝐹‘𝑤)))
Theorem	evthicc2 24633*	Combine ivthicc 24631 with evthicc 24632 to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ ran 𝐹 = (𝑥[,]𝑦))
Theorem	cniccbdd 24634*	A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥)
13.2  Integrals
13.2.1  Lebesgue measure
Syntax	covol 24635	Extend class notation with the outer Lebesgue measure.
class vol*
Syntax	cvol 24636	Extend class notation with the Lebesgue measure.
class vol
Definition	df-ovol 24637*	Define the outer Lebesgue measure for subsets of the reals. Here 𝑓 is a function from the positive integers to pairs ⟨𝑎, 𝑏⟩ with 𝑎 ≤ 𝑏, and the outer volume of the set 𝑥 is the infimum over all such functions such that the union of the open intervals (𝑎, 𝑏) covers 𝑥 of the sum of 𝑏 − 𝑎. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.)
⊢ vol* = (𝑥 ∈ 𝒫 ℝ ↦ inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < ))
Definition	df-vol 24638*	Define the Lebesgue measure, which is just the outer measure with a peculiar domain of definition. The property of being Lebesgue-measurable can be expressed as 𝐴 ∈ dom vol. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ vol = (vol* ↾ {𝑥 ∣ ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))})
Theorem	ovolfcl 24639	Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑁)) ≤ (2nd ‘(𝐹‘𝑁))))
Theorem	ovolfioo 24640*	Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛)))))
Theorem	ovolficc 24641*	Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ([,] ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛)))))
Theorem	ovolficcss 24642	Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
Theorem	ovolfsval 24643	The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐺‘𝑁) = ((2nd ‘(𝐹‘𝑁)) − (1st ‘(𝐹‘𝑁))))
Theorem	ovolfsf 24644	Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    ⇒   ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺:ℕ⟶(0[,)+∞))
Theorem	ovolsf 24645	Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    &   ⊢ 𝑆 = seq1( + , 𝐺)    ⇒   ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
Theorem	ovolval 24646*	The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) = inf(𝑀, ℝ*, < ))
Theorem	elovolmlem 24647	Lemma for elovolm 24648 and related theorems. (Contributed by BJ, 23-Jul-2022.)
⊢ (𝐹 ∈ ((𝐴 ∩ (ℝ × ℝ)) ↑m ℕ) ↔ 𝐹:ℕ⟶(𝐴 ∩ (ℝ × ℝ)))
Theorem	elovolm 24648*	Elementhood in the set 𝑀 of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )))
Theorem	elovolmr 24649*	Sufficient condition for elementhood in the set 𝑀. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀)
Theorem	ovolmge0 24650*	The set 𝑀 is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝐵 ∈ 𝑀 → 0 ≤ 𝐵)
Theorem	ovolcl 24651	The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*)
Theorem	ovollb 24652	The outer volume is a lower bound on the sum of all interval coverings of 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolgelb 24653*	The outer volume is the greatest lower bound on the sum of all interval coverings of 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝑔))    ⇒   ⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + 𝐵)))
Theorem	ovolge0 24654	The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ (𝐴 ⊆ ℝ → 0 ≤ (vol*‘𝐴))
Theorem	ovolf 24655	The domain and range of the outer volume function. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.)
⊢ vol*:𝒫 ℝ⟶(0[,]+∞)
Theorem	ovollecl 24656	If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (vol*‘𝐴) ≤ 𝐵) → (vol*‘𝐴) ∈ ℝ)
Theorem	ovolsslem 24657*	Lemma for ovolss 24658. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    &   ⊢ 𝑁 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵))
Theorem	ovolss 24658	The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵))
Theorem	ovolsscl 24659	If a set is contained in another of bounded measure, it too is bounded. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → (vol*‘𝐴) ∈ ℝ)
Theorem	ovolssnul 24660	A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘𝐴) = 0)
Theorem	ovollb2lem 24661*	Lemma for ovollb2 24662. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩)    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
Theorem	ovollb2 24662	It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb 24652). (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolctb 24663	The volume of a denumerable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≈ ℕ) → (vol*‘𝐴) = 0)
Theorem	ovolq 24664	The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (vol*‘ℚ) = 0
Theorem	ovolctb2 24665	The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (vol*‘𝐴) = 0)
Theorem	ovol0 24666	The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (vol*‘∅) = 0
Theorem	ovolfi 24667	A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ) → (vol*‘𝐴) = 0)
Theorem	ovolsn 24668	A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0)
Theorem	ovolunlem1a 24669*	Lemma for ovolun 24672. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))    &   ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))    &   ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Theorem	ovolunlem1 24670*	Lemma for ovolun 24672. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))    &   ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))    &   ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))    ⇒   ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Theorem	ovolunlem2 24671	Lemma for ovolun 24672. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))    &   ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Theorem	ovolun 24672	The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 24678, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵)))
Theorem	ovolunnul 24673	Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴))
Theorem	ovolfiniun 24674*	The Lebesgue outer measure function is finitely sub-additive. Finite sum version. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘∪ 𝑘 ∈ 𝐴 𝐵) ≤ Σ𝑘 ∈ 𝐴 (vol*‘𝐵))
Theorem	ovoliunlem1 24675*	Lemma for ovoliun 24678. (Contributed by Mario Carneiro, 12-Jun-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹‘𝑛)))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))))    &   ⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿)    ⇒   ⊢ (𝜑 → (𝑈‘𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Theorem	ovoliunlem2 24676*	Lemma for ovoliun 24678. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹‘𝑛)))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))))    &   ⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Theorem	ovoliunlem3 24677*	Lemma for ovoliun 24678. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Theorem	ovoliun 24678*	The Lebesgue outer measure function is countably sub-additive. (Many books allow +∞ as a value for one of the sets in the sum, but in our setup we can't do arithmetic on infinity, and in any case the volume of a union containing an infinitely large set is already infinitely large by monotonicity ovolss 24658, so we need not consider this case here, although we do allow the sum itself to be infinite.) (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
Theorem	ovoliun2 24679*	The Lebesgue outer measure function is countably sub-additive. (This version is a little easier to read, but does not allow infinite values like ovoliun 24678.) (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴))
Theorem	ovoliunnul 24680*	A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015.)
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)
Theorem	shft2rab 24681*	If 𝐵 is a shift of 𝐴 by 𝐶, then 𝐴 is a shift of 𝐵 by -𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.) (Revised by Mario Carneiro, 6-Apr-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    ⇒   ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ (𝑦 − -𝐶) ∈ 𝐵})
Theorem	ovolshftlem1 24682*	Lemma for ovolshft 24684. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    &   ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)⟩)    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    ⇒   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀)
Theorem	ovolshftlem2 24683*	Lemma for ovolshft 24684. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    &   ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, < ))} ⊆ 𝑀)
Theorem	ovolshft 24684*	The Lebesgue outer measure function is shift-invariant. (Contributed by Mario Carneiro, 22-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    ⇒   ⊢ (𝜑 → (vol*‘𝐴) = (vol*‘𝐵))
Theorem	sca2rab 24685*	If 𝐵 is a scale of 𝐴 by 𝐶, then 𝐴 is a scale of 𝐵 by 1 / 𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    ⇒   ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ ((1 / 𝐶) · 𝑦) ∈ 𝐵})
Theorem	ovolscalem1 24686*	Lemma for ovolsca 24688. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)⟩)    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))    ⇒   ⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
Theorem	ovolscalem2 24687*	Lemma for ovolshft 24684. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶))
Theorem	ovolsca 24688*	The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐵) = ((vol*‘𝐴) / 𝐶))
Theorem	ovolicc1 24689*	The measure of a closed interval is lower bounded by its length. (Contributed by Mario Carneiro, 13-Jun-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩))    ⇒   ⊢ (𝜑 → (vol*‘(𝐴[,]𝐵)) ≤ (𝐵 − 𝐴))
Theorem	ovolicc2lem1 24690*	Lemma for ovolicc2 24695. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋))))))
Theorem	ovolicc2lem2 24691*	Lemma for ovolicc2 24695. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    &   ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))    &   ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}    ⇒   ⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵)
Theorem	ovolicc2lem3 24692*	Lemma for ovolicc2 24695. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    &   ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))    &   ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}    ⇒   ⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃))))))
Theorem	ovolicc2lem4 24693*	Lemma for ovolicc2 24695. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by AV, 17-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    &   ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))    &   ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}    &   ⊢ 𝑀 = inf(𝑊, ℝ, < )    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolicc2lem5 24694*	Lemma for ovolicc2 24695. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolicc2 24695*	The measure of a closed interval is upper bounded by its length. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)((𝐴[,]𝐵) ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (vol*‘(𝐴[,]𝐵)))
Theorem	ovolicc 24696	The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
Theorem	ovolicopnf 24697	The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝐴 ∈ ℝ → (vol*‘(𝐴[,)+∞)) = +∞)
Theorem	ovolre 24698	The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (vol*‘ℝ) = +∞
Theorem	ismbl 24699*	The predicate "𝐴 is Lebesgue-measurable". A set is measurable if it splits every other set 𝑥 in a "nice" way, that is, if the measure of the pieces 𝑥 ∩ 𝐴 and 𝑥 ∖ 𝐴 sum up to the measure of 𝑥 (assuming that the measure of 𝑥 is a real number, so that this addition makes sense). (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))))))
Theorem	ismbl2 24700*	From ovolun 24672, it suffices to show that the measure of 𝑥 is at least the sum of the measures of 𝑥 ∩ 𝐴 and 𝑥 ∖ 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))))