Home | Metamath
Proof Explorer Theorem List (p. 430 of 450) | < 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: | Metamath Proof Explorer
(1-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hoidifhspdmvle 42901* | The dimensional volume of the difference of a half-open interval and a half-space is less than or equal to the dimensional volume of the whole half-open interval. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ 𝐷 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → (((𝐷‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ≤ (𝐴(𝐿‘𝑋)𝐵)) | ||
Theorem | voncmpl 42902 | The Lebesgue measure is complete. See Definition 112Df of [Fremlin1] p. 19. This is an observation written after Definition 115E of [Fremlin1] p. 31 (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐸 ∈ dom (voln‘𝑋)) & ⊢ (𝜑 → ((voln‘𝑋)‘𝐸) = 0) & ⊢ (𝜑 → 𝐹 ⊆ 𝐸) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑆) | ||
Theorem | hoiqssbllem1 42903* | The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑖𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐶:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐷:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ⇒ ⊢ (𝜑 → 𝑌 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) | ||
Theorem | hoiqssbllem2 42904* | The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑖𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐶:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐷:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) | ||
Theorem | hoiqssbllem3 42905* | A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) | ||
Theorem | hoiqssbl 42906* | A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) | ||
Theorem | hspmbllem1 42907* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (a) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) & ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵))) | ||
Theorem | hspmbllem2 42908* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸)) & ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ) & ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) & ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) & ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) ⇒ ⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸)) | ||
Theorem | hspmbllem3 42909* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. This proof handles the non-trivial cases (nonzero dimension and finite outer measure) (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) & ⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) & ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})) & ⊢ 𝐵 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑘)))) & ⊢ 𝑇 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑘)))) ⇒ ⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) +𝑒 ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln*‘𝑋)‘𝐴)) | ||
Theorem | hspmbl 42910* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) ∈ dom (voln‘𝑋)) | ||
Theorem | hoimbllem 42911* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∈ 𝑆) | ||
Theorem | hoimbl 42912* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∈ 𝑆) | ||
Theorem | opnvonmbllem1 42913* | The half-open interval expressed using a composition of a function (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑖𝜑 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐶:𝑋⟶ℚ) & ⊢ (𝜑 → 𝐷:𝑋⟶ℚ) & ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐺) & ⊢ (𝜑 → 𝑌 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) & ⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} & ⊢ 𝐻 = (𝑖 ∈ 𝑋 ↦ 〈(𝐶‘𝑖), (𝐷‘𝑖)〉) ⇒ ⊢ (𝜑 → ∃ℎ ∈ 𝐾 𝑌 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) | ||
Theorem | opnvonmbllem2 42914* | An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) & ⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑆) | ||
Theorem | opnvonmbl 42915 | An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑆) | ||
Theorem | opnssborel 42916 | Open sets of a generalized real Euclidean space are Borel sets (notice that this theorem is even more general, because 𝑋 is not required to be a set). (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ 𝐴 = (TopOpen‘(ℝ^‘𝑋)) & ⊢ 𝐵 = (SalGen‘𝐴) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | borelmbl 42917 | All Borel subsets of the n-dimensional Real numbers are Lebesgue measurable. This is Proposition 115G (b) of [Fremlin1] p. 32. See also Definition 111G (d) of [Fremlin1] p. 13. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ 𝐵 = (SalGen‘(TopOpen‘(ℝ^‘𝑋))) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝑆) | ||
Theorem | volicorege0 42918 | The Lebesgue measure of a left-closed right-open interval with real bounds, is a nonnegative real number. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) ∈ (0[,)+∞)) | ||
Theorem | isvonmbl 42919* | The predicate "𝐴 is measurable w.r.t. the n-dimensional Lebesgue measure". 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 𝑥. Definition 114E of [Fremlin1] p. 25. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐸 ∈ dom (voln‘𝑋) ↔ (𝐸 ⊆ (ℝ ↑m 𝑋) ∧ ∀𝑎 ∈ 𝒫 (ℝ ↑m 𝑋)(((voln*‘𝑋)‘(𝑎 ∩ 𝐸)) +𝑒 ((voln*‘𝑋)‘(𝑎 ∖ 𝐸))) = ((voln*‘𝑋)‘𝑎)))) | ||
Theorem | mblvon 42920 | The n-dimensional Lebesgue measure of a measurable set is the same as its n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ dom (voln‘𝑋)) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐴) = ((voln*‘𝑋)‘𝐴)) | ||
Theorem | vonmblss 42921 | n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → dom (voln‘𝑋) ⊆ 𝒫 (ℝ ↑m 𝑋)) | ||
Theorem | volico2 42922 | The measure of left-closed right-open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) = if(𝐴 ≤ 𝐵, (𝐵 − 𝐴), 0)) | ||
Theorem | vonmblss2 42923 | n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ dom (voln‘𝑋)) ⇒ ⊢ (𝜑 → 𝑌 ⊆ (ℝ ↑m 𝑋)) | ||
Theorem | ovolval2lem 42924* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ⇒ ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐹)) = ran (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘)))) | ||
Theorem | ovolval2 42925* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^. See ovolval 24073 for an alternative expression. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((abs ∘ − ) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | ovnsubadd2lem 42926* | (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∪ 𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵))) | ||
Theorem | ovnsubadd2 42927 | (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∪ 𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵))) | ||
Theorem | ovolval3 42928* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^ and vol ∘ (,). See ovolval 24073 and ovolval2 42925 for alternative expressions. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | ovnsplit 42929 | The n-dimensional Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ (((voln*‘𝑋)‘(𝐴 ∩ 𝐵)) +𝑒 ((voln*‘𝑋)‘(𝐴 ∖ 𝐵)))) | ||
Theorem | ovolval4lem1 42930* | |- ( ( ph /\ n e. A ) -> ( ( (,) o. G ) 𝑛) = (((,) ∘ 𝐹) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) & ⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⇒ ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))) | ||
Theorem | ovolval4lem2 42931* | The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 42928, but here 𝑓 is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉) ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | ovolval4 42932* | The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 42928, but here 𝑓 may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | ovolval5lem1 42933* | ⊢ (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛) ))(,)𝐵)))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵) ))) +𝑒 𝑊)) (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ+) & ⊢ 𝐶 = {𝑛 ∈ ℕ ∣ 𝐴 < 𝐵} ⇒ ⊢ (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) | ||
Theorem | ovolval5lem2 42934* | |- ( ( ph /\ n e. NN ) -> <. ( ( 1st (𝐹 n ) ) - ( W / ( 2 ^ n ) ) ) , ( 2nd (𝐹 n ) ) >. e. ( RR X. RR ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} & ⊢ (𝜑 → 𝑌 = (Σ^‘((vol ∘ [,)) ∘ 𝐹))) & ⊢ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)) & ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ([,) ∘ 𝐹)) & ⊢ (𝜑 → 𝑊 ∈ ℝ+) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹‘𝑛))〉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊)) | ||
Theorem | ovolval5lem3 42935* | The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))} & ⊢ 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⇒ ⊢ inf(𝑄, ℝ*, < ) = inf(𝑀, ℝ*, < ) | ||
Theorem | ovolval5 42936* | The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | ovnovollem1 42937* | if 𝐹 is a cover of 𝐵 in ℝ, then 𝐼 is the corresponding cover in the space of 1-dimensional reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ) ↑m ℕ)) & ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {〈𝐴, (𝐹‘𝑗)〉}) & ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹)) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹))) ⇒ ⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | ||
Theorem | ovnovollem2 42938* | if 𝐼 is a cover of (𝐵 ↑m {𝐴}) in ℝ^1, then 𝐹 is the corresponding cover in the reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)) & ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) & ⊢ (𝜑 → 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) & ⊢ 𝐹 = (𝑗 ∈ ℕ ↦ ((𝐼‘𝑗)‘𝐴)) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))) | ||
Theorem | ovnovollem3 42939* | The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} & ⊢ 𝑁 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → ((voln*‘{𝐴})‘(𝐵 ↑m {𝐴})) = (vol*‘𝐵)) | ||
Theorem | ovnovol 42940 | The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) ⇒ ⊢ (𝜑 → ((voln*‘{𝐴})‘(𝐵 ↑m {𝐴})) = (vol*‘𝐵)) | ||
Theorem | vonvolmbllem 42941* | If a subset 𝐵 of real numbers is Lebesgue measurable, then its corresponding 1-dimensional set is measurable w.r.t. the n-dimensional Lebesgue measure, (with 𝑛 equal to 1). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) & ⊢ (𝜑 → 𝑋 ⊆ (ℝ ↑m {𝐴})) & ⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⇒ ⊢ (𝜑 → (((voln*‘{𝐴})‘(𝑋 ∩ (𝐵 ↑m {𝐴}))) +𝑒 ((voln*‘{𝐴})‘(𝑋 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑋)) | ||
Theorem | vonvolmbl 42942 | A subset of Real numbers is Lebesgue measurable if and only if its corresponding 1-dimensional set is measurable w.r.t. the 1-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) ⇒ ⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ∈ dom (voln‘{𝐴}) ↔ 𝐵 ∈ dom vol)) | ||
Theorem | vonvol 42943 | The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ dom vol) ⇒ ⊢ (𝜑 → ((voln‘{𝐴})‘(𝐵 ↑m {𝐴})) = (vol‘𝐵)) | ||
Theorem | vonvolmbl2 42944* | A subset 𝑋 of the space of 1-dimensional Real numbers is Lebesgue measurable if and only if its projection 𝑌 on the Real numbers is Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑓𝑌 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ (ℝ ↑m {𝐴})) & ⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⇒ ⊢ (𝜑 → (𝑋 ∈ dom (voln‘{𝐴}) ↔ 𝑌 ∈ dom vol)) | ||
Theorem | vonvol2 42945* | The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑓𝑌 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ dom (voln‘{𝐴})) & ⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⇒ ⊢ (𝜑 → ((voln‘{𝐴})‘𝑋) = (vol‘𝑌)) | ||
Theorem | hoimbl2 42946* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 (𝐴[,)𝐵) ∈ 𝑆) | ||
Theorem | voncl 42947 | The Lebesgue measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐴) ∈ (0[,]+∞)) | ||
Theorem | vonhoi 42948* | The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). A direct consequence of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | ||
Theorem | vonxrcl 42949 | The Lebesgue measure of a set is an extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐴) ∈ ℝ*) | ||
Theorem | ioosshoi 42950 | A n-dimensional open interval is a subset of the half-open interval with the same bounds. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ X𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)𝐵) | ||
Theorem | vonn0hoi 42951* | The Lebesgue outer measure of a multidimensional half-open interval when the dimension of the space is nonzero. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | ||
Theorem | von0val 42952 | The Lebesgue measure (for the zero dimensional space of reals) of every measurable set is zero. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ dom (voln‘∅)) ⇒ ⊢ (𝜑 → ((voln‘∅)‘𝐴) = 0) | ||
Theorem | vonhoire 42953* | The Lebesgue measure of a n-dimensional half-open interval is a real number. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘X𝑘 ∈ 𝑋 (𝐴[,)𝐵)) ∈ ℝ) | ||
Theorem | iinhoiicclem 42954* | A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛)))) ⇒ ⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,]𝐵)) | ||
Theorem | iinhoiicc 42955* | A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) = X𝑘 ∈ 𝑋 (𝐴[,]𝐵)) | ||
Theorem | iunhoiioolem 42956* | A n-dimensional open interval expressed as the indexed union of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) & ⊢ 𝐶 = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) ⇒ ⊢ (𝜑 → 𝐹 ∈ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) | ||
Theorem | iunhoiioo 42957* | A n-dimensional open interval expressed as the indexed union of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) | ||
Theorem | ioovonmbl 42958* | Any n-dimensional open interval is Lebesgue measurable. This is the first statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ 𝑆) | ||
Theorem | iccvonmbllem 42959* | Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑖 ∈ 𝑋 ↦ ((𝐴‘𝑖) − (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑖 ∈ 𝑋 ↦ ((𝐵‘𝑖) + (1 / 𝑛)))) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,](𝐵‘𝑖)) ∈ 𝑆) | ||
Theorem | iccvonmbl 42960* | Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,](𝐵‘𝑖)) ∈ 𝑆) | ||
Theorem | vonioolem1 42961* | The sequence of the measures of the half-open intervals converges to the measure of their union. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) & ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) & ⊢ 𝐸 = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) & ⊢ 𝑁 = ((⌊‘(1 / 𝐸)) + 1) & ⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) | ||
Theorem | vonioolem2 42962* | The n-dimensional Lebesgue measure of open intervals. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) | ||
Theorem | vonioo 42963* | The n-dimensional Lebesgue measure of an open interval. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | ||
Theorem | vonicclem1 42964* | The sequence of the measures of the half-open intervals converges to the measure of their intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) | ||
Theorem | vonicclem2 42965* | The n-dimensional Lebesgue measure of closed intervals. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘)) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) | ||
Theorem | vonicc 42966* | The n-dimensional Lebesgue measure of a closed interval. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | ||
Theorem | snvonmbl 42967 | A n-dimensional singleton is Lebesgue measurable. This is the first statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → {𝐴} ∈ dom (voln‘𝑋)) | ||
Theorem | vonn0ioo 42968* | The n-dimensional Lebesgue measure of an open interval when the dimension of the space is nonzero. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | ||
Theorem | vonn0icc 42969* | The n-dimensional Lebesgue measure of a closed interval, when the dimension of the space is nonzero. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,](𝐵‘𝑘)))) | ||
Theorem | ctvonmbl 42970 | Any n-dimensional countable set is Lebesgue measurable. This is the second statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐴 ≼ ω) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom (voln‘𝑋)) | ||
Theorem | vonn0ioo2 42971* | The n-dimensional Lebesgue measure of an open interval when the dimension of the space is nonzero. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 (vol‘(𝐴(,)𝐵))) | ||
Theorem | vonsn 42972 | The n-dimensional Lebesgue measure of a singleton is zero. This is the first statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘{𝐴}) = 0) | ||
Theorem | vonn0icc2 42973* | The n-dimensional Lebesgue measure of a closed interval, when the dimension of the space is nonzero. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 (𝐴[,]𝐵) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 (vol‘(𝐴[,]𝐵))) | ||
Theorem | vonct 42974 | The n-dimensional Lebesgue measure of any countable set is zero. This is the second statement in Proposition 115G (e) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐴 ≼ ω) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐴) = 0) | ||
Theorem | vitali2 42975 | There are non-measurable sets (the Axiom of Choice is used, in the invoked weth 9916). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ dom vol ⊊ 𝒫 ℝ | ||
Proofs for most of the theorems in section 121 of [Fremlin1]. Real-valued functions are considered, and measurability is defined with respect to an arbitrary sigma-algebra. When the sigma-algebra on the domain is the Lebesgue measure on the reals, then all real-valued measurable functions in the sense of df-mbf 24219 are also sigma-measurable, but the definition in this section considers as measurable functions, some that are not measurable in the sense of df-mbf 24219 (see mbfpsssmf 43058 and smfmbfcex 43035). | ||
Syntax | csmblfn 42976 | Extend class notation with the class of real-valued measurable functions w.r.t. sigma-algebras. |
class SMblFn | ||
Definition | df-smblfn 42977* | Define a real-valued measurable function w.r.t. a given sigma-algebra. See Definition 121C of [Fremlin1] p. 36 and Definition 135E (b) of [Fremlin1] p. 80 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ SMblFn = (𝑠 ∈ SAlg ↦ {𝑓 ∈ (ℝ ↑pm ∪ 𝑠) ∣ ∀𝑎 ∈ ℝ (◡𝑓 “ (-∞(,)𝑎)) ∈ (𝑠 ↾t dom 𝑓)}) | ||
Theorem | pimltmnf2 42978* | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -∞, is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < -∞} = ∅) | ||
Theorem | preimagelt 42979* | The preimage of a right-open, unbounded below interval, is the complement of a left-closed unbounded above interval. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) = {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) | ||
Theorem | preimalegt 42980* | The preimage of a left-open, unbounded above interval, is the complement of a right-closed unbounded below interval. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) | ||
Theorem | pimconstlt0 42981* | Given a constant function, its preimage with respect to an unbounded below, open interval, with upper bound less than or equal to the constant, is the empty set. Second part of Proposition 121E (a) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐶} = ∅) | ||
Theorem | pimconstlt1 42982* | Given a constant function, its preimage with respect to an unbounded below, open interval, with upper bound larger than the constant, is the whole domain. First part of Proposition 121E (a) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐶} = 𝐴) | ||
Theorem | pimltpnf 42983* | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +∞, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < +∞} = 𝐴) | ||
Theorem | pimgtpnf2 42984* | Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound +∞, is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ +∞ < (𝐹‘𝑥)} = ∅) | ||
Theorem | salpreimagelt 42985* | If all the preimages of left-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (iv) implies (i) in Proposition 121B of [Fremlin1] p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑎𝜑 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ 𝐴 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝑎 ≤ 𝐵} ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ∈ 𝑆) | ||
Theorem | pimrecltpos 42986 | The preimage of an unbounded below, open interval, with positive upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} = ({𝑥 ∈ 𝐴 ∣ (1 / 𝐶) < 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ 𝐵 < 0})) | ||
Theorem | salpreimalegt 42987* | If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of left-open, unbounded above intervals, belong to the sigma-algebra. (ii) implies (iii) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑎𝜑 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ 𝐴 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎} ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} ∈ 𝑆) | ||
Theorem | pimiooltgt 42988* | The preimage of an open interval is the intersection of the preimage of an unbounded below open interval and an unbounded above open interval. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐿 ∈ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} = ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) | ||
Theorem | preimaicomnf 42989* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (◡𝐹 “ (-∞[,)𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐵}) | ||
Theorem | pimltpnf2 42990* | Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +∞, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < +∞} = 𝐴) | ||
Theorem | pimgtmnf2 42991* | Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -∞, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < (𝐹‘𝑥)} = 𝐴) | ||
Theorem | pimdecfgtioc 42992* | Given a nonincreasing function, the preimage of an unbounded above, open interval, when the supremum of the preimage belongs to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} & ⊢ 𝑆 = sup(𝑌, ℝ*, < ) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) & ⊢ 𝐼 = (-∞(,]𝑆) ⇒ ⊢ (𝜑 → 𝑌 = (𝐼 ∩ 𝐴)) | ||
Theorem | pimincfltioc 42993* | Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage belongs to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝑅} & ⊢ 𝑆 = sup(𝑌, ℝ*, < ) & ⊢ (𝜑 → 𝑆 ∈ 𝑌) & ⊢ 𝐼 = (-∞(,]𝑆) ⇒ ⊢ (𝜑 → 𝑌 = (𝐼 ∩ 𝐴)) | ||
Theorem | pimdecfgtioo 42994* | Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage does not belong to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} & ⊢ 𝑆 = sup(𝑌, ℝ*, < ) & ⊢ (𝜑 → ¬ 𝑆 ∈ 𝑌) & ⊢ 𝐼 = (-∞(,)𝑆) ⇒ ⊢ (𝜑 → 𝑌 = (𝐼 ∩ 𝐴)) | ||
Theorem | pimincfltioo 42995* | Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage does not belong to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝑅} & ⊢ 𝑆 = sup(𝑌, ℝ*, < ) & ⊢ (𝜑 → ¬ 𝑆 ∈ 𝑌) & ⊢ 𝐼 = (-∞(,)𝑆) ⇒ ⊢ (𝜑 → 𝑌 = (𝐼 ∩ 𝐴)) | ||
Theorem | preimaioomnf 42996* | Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐵}) | ||
Theorem | preimageiingt 42997* | A preimage of a left-closed, unbounded above interval, expressed as an indexed intersection of preimages of open, unbounded above intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} = ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) | ||
Theorem | preimaleiinlt 42998* | A preimage of a left-open, right-closed, unbounded below interval, expressed as an indexed intersection of preimages of open, unbound below intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} = ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ 𝐵 < (𝐶 + (1 / 𝑛))}) | ||
Theorem | pimgtmnf 42999* | Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -∞, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} = 𝐴) | ||
Theorem | pimrecltneg 43000 | The preimage of an unbounded below, open interval, with negative upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |