P. 469 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46801-46900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iccvonmbl 46801*	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 46802*	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 46803*	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 46804*	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 46805*	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 46806*	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 46807*	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 46808	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 46809*	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 46810*	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 46811	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 46812*	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 46813	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 46814*	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 46815	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 46816	There are non-measurable sets (the Axiom of Choice is used, in the invoked weth 10393). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ dom vol ⊊ 𝒫 ℝ
21.43.19.6  Measurable functions 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 25548 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 25548 (see mbfpsssmf 46905 and smfmbfcex 46882).
Syntax	csmblfn 46817	Extend class notation with the class of real-valued measurable functions w.r.t. sigma-algebras.
class SMblFn
Definition	df-smblfn 46818*	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	pimltmnf2f 46819	Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -∞, is the empty set. (Contributed by Glauco Siliprandi, 15-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < -∞} = ∅)
Theorem	pimltmnf2 46820*	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.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < -∞} = ∅)
Theorem	preimagelt 46821*	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 46822*	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 46823*	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 46824*	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	pimltpnff 46825	Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +∞, is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < +∞} = 𝐴)
Theorem	pimltpnf 46826*	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.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < +∞} = 𝐴)
Theorem	pimgtpnf2f 46827	Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound +∞, is the empty set. (Contributed by Glauco Siliprandi, 15-Dec-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ +∞ < (𝐹‘𝑥)} = ∅)
Theorem	pimgtpnf2 46828*	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.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ +∞ < (𝐹‘𝑥)} = ∅)
Theorem	salpreimagelt 46829*	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 46830	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 46831*	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 46832*	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 46833*	Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (◡𝐹 “ (-∞[,)𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐵})
Theorem	pimltpnf2f 46834	Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +∞, is the whole domain. (Contributed by Glauco Siliprandi, 15-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < +∞} = 𝐴)
Theorem	pimltpnf2 46835*	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.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < +∞} = 𝐴)
Theorem	pimgtmnf2 46836*	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 46837*	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 46838*	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 46839*	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 46840*	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 46841*	Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝐵)) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝐵})
Theorem	preimageiingt 46842*	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 46843*	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	pimgtmnff 46844	Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -∞, is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} = 𝐴)
Theorem	pimgtmnf 46845*	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.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} = 𝐴)
Theorem	pimrecltneg 46846	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)})
Theorem	salpreimagtge 46847*	If all the preimages of left-open, unbounded above intervals, belong to a sigma-algebra, then all the preimages of left-closed, unbounded above intervals, belong to the sigma-algebra. (iii) implies (iv) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝑎 < 𝐵} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ∈ 𝑆)
Theorem	salpreimaltle 46848*	If all the preimages of right-open, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-closed, unbounded below intervals, belong to the sigma-algebra. (i) implies (ii) in Proposition 121B of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ∈ 𝑆)
Theorem	issmflem 46849*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
Theorem	issmf 46850*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
Theorem	salpreimalelt 46851*	If all the preimages of right-closed, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (ii) implies (i) in Proposition 121B of [Fremlin1] p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐴 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝑎} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ∈ 𝑆)
Theorem	salpreimagtlt 46852*	If all the preimages of lef-open, unbounded above intervals, belong to a sigma-algebra, then all the preimages of right-open, unbounded below intervals, belong to the sigma-algebra. (iii) implies (i) in Proposition 121B of [Fremlin1] p. 36. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐴 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝑎 < 𝐵} ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ∈ 𝑆)
Theorem	smfpreimalt 46853*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	smff 46854	A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
Theorem	smfdmss 46855	The domain of a function measurable w.r.t. to a sigma-algebra, is a subset of the set underlying the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)
Theorem	issmff 46856*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (i) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))))
Theorem	issmfd 46857*	A sufficient condition for "𝐹 being a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	smfpreimaltf 46858*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	issmfdf 46859*	A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	sssmf 46860	The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ (SMblFn‘𝑆))
Theorem	mbfresmf 46861	A real-valued measurable function is a sigma-measurable function (w.r.t. the Lebesgue measure on the Reals). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)    &   ⊢ 𝑆 = dom vol    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	cnfsmf 46862	A continuous function is measurable. Proposition 121D (b) of [Fremlin1] p. 36 is a special case of this theorem, where the topology on the domain is induced by the standard topology on n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t dom 𝐹) Cn 𝐾))    &   ⊢ 𝑆 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	incsmflem 46863*	A nondecreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) < 𝑅}    &   ⊢ 𝐶 = sup(𝑌, ℝ*, < )    &   ⊢ 𝐷 = (-∞(,)𝐶)    &   ⊢ 𝐸 = (-∞(,]𝐶)    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ 𝐵 𝑌 = (𝑏 ∩ 𝐴))
Theorem	incsmf 46864*	A real-valued, nondecreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵))
Theorem	smfsssmf 46865	If a function is measurable w.r.t. to a sigma-algebra, then it is measurable w.r.t. to a larger sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑅 ∈ SAlg)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑅 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑅))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	issmflelem 46866*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (ii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≤ 𝑎} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	issmfle 46867*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all right-closed intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be b subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (ii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≤ 𝑎} ∈ (𝑆 ↾t 𝐷))))
Theorem	smfpimltmpt 46868*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∈ (𝑆 ↾t 𝐴))
Theorem	smfpimltxr 46869*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) < 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	issmfdmpt 46870*	A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑎} ∈ (𝑆 ↾t 𝐴))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))
Theorem	smfconst 46871*	Given a sigma-algebra over a base set X, every partial real-valued constant function is measurable. Proposition 121E (a) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	sssmfmpt 46872*	The restriction of a sigma-measurable function is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) ∈ (SMblFn‘𝑆))
Theorem	cnfrrnsmf 46873	A function, continuous from the standard topology on the space of n-dimensional reals to the standard topology on the reals, is Borel measurable. Proposition 121D (b) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝑋))    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t dom 𝐹) Cn 𝐾))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵))
Theorem	smfid 46874*	The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑥) ∈ (SMblFn‘𝐵))
Theorem	bormflebmf 46875	A Borel measurable function is Lebesgue measurable. Proposition 121D (a) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐵 = (SalGen‘(TopOpen‘(ℝ^‘𝑋)))    &   ⊢ 𝐿 = dom (voln‘𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐿))
Theorem	smfpreimale 46876*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of a closed interval unbounded below is in the subspace sigma-algebra induced by its domain. See Proposition 121B (ii) of [Fremlin1] p. 35 (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	issmfgtlem 46877*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all left-open intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (iii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ (𝜑 → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	issmfgt 46878*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all left-open intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be b subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (iii) of [Fremlin1] p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))))
Theorem	issmfled 46879*	A sufficient condition for "𝐹 being a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≤ 𝑎} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	smfpimltxrmptf 46880*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∈ (𝑆 ↾t 𝐴))
Theorem	smfpimltxrmpt 46881*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∈ (𝑆 ↾t 𝐴))
Theorem	smfmbfcex 46882*	A constant function, with non-lebesgue-measurable domain is a sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) but it is not a measurable functions ( w.r.t. to df-mbf 25548). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑆 = dom vol    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ 0)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ∧ ¬ 𝐹 ∈ MblFn))
Theorem	issmfgtd 46883*	A sufficient condition for "𝐹 being a measurable function w.r.t. to the sigma-algebra 𝑆". (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ 𝐷 ∣ 𝑎 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	smfpreimagt 46884*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ 𝐴 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))
Theorem	smfaddlem1 46885*	Given the sum of two functions, the preimage of an unbounded below, open interval, expressed as the countable union of intersections of preimages of both functions. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})    ⇒   ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} = ∪ 𝑝 ∈ ℚ ∪ 𝑞 ∈ (𝐾‘𝑝){𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 < 𝑝 ∧ 𝐷 < 𝑞)})
Theorem	smfaddlem2 46886*	The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ 𝐾 = (𝑝 ∈ ℚ ↦ {𝑞 ∈ ℚ ∣ (𝑝 + 𝑞) < 𝑅})    ⇒   ⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 + 𝐷) < 𝑅} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶)))
Theorem	smfadd 46887*	The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of [Fremlin1] p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ (𝐵 + 𝐷)) ∈ (SMblFn‘𝑆))
Theorem	decsmflem 46888*	A nonincreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)}    &   ⊢ 𝐶 = sup(𝑌, ℝ*, < )    &   ⊢ 𝐷 = (-∞(,)𝐶)    &   ⊢ 𝐸 = (-∞(,]𝐶)    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ 𝐵 𝑌 = (𝑏 ∩ 𝐴))
Theorem	decsmf 46889*	A real-valued, nonincreasing function is Borel measurable. Proposition 121D (c) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝐵))
Theorem	smfpreimagtf 46890*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ 𝐴 < (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))
Theorem	issmfgelem 46891*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all left-closed intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be a subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (iv) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑎𝜑    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐷 ⊆ ∪ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ (𝜑 → ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
Theorem	issmfge 46892*	The predicate "𝐹 is a real-valued measurable function w.r.t. to the sigma-algebra 𝑆". A function is measurable iff the preimages of all left-closed intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of 𝐹 is required to be b subset of the underlying set of 𝑆. Definition 121C of [Fremlin1] p. 36, and Proposition 121B (iv) of [Fremlin1] p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → (𝐹 ∈ (SMblFn‘𝑆) ↔ (𝐷 ⊆ ∪ 𝑆 ∧ 𝐹:𝐷⟶ℝ ∧ ∀𝑎 ∈ ℝ {𝑥 ∈ 𝐷 ∣ 𝑎 ≤ (𝐹‘𝑥)} ∈ (𝑆 ↾t 𝐷))))
Theorem	smflimlem1 46893*	Lemma for the proof that the limit of a sequence of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves that (𝐷 ∩ 𝐼) is in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟)    ⇒   ⊢ (𝜑 → (𝐷 ∩ 𝐼) ∈ (𝑆 ↾t 𝐷))
Theorem	smflimlem2 46894*	Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ⊆ (𝐷 ∩ 𝐼))
Theorem	smflimlem3 46895*	The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑃) → (𝐶‘𝑦) ∈ 𝑦)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐷 ∩ 𝐼))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ+)    &   ⊢ (𝜑 → (1 / 𝐾) < 𝑌)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ 𝑍 ∀𝑖 ∈ (ℤ≥‘𝑚)(𝑋 ∈ dom (𝐹‘𝑖) ∧ ((𝐹‘𝑖)‘𝑋) < (𝐴 + 𝑌)))
Theorem	smflimlem4 46896*	Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟)    ⇒   ⊢ (𝜑 → (𝐷 ∩ 𝐼) ⊆ {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴})
Theorem	smflimlem5 46897*	Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    &   ⊢ 𝐻 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ (𝐶‘(𝑚𝑃𝑘)))    &   ⊢ 𝐼 = ∩ 𝑘 ∈ ℕ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)(𝑚𝐻𝑘)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ran 𝑃) → (𝐶‘𝑟) ∈ 𝑟)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	smflimlem6 46898*	Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))})    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	smflim 46899*	The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of [Fremlin1] p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of [Fremlin1] p. 39 ). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ }    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	nsssmfmbflem 46900*	The sigma-measurable functions (w.r.t. the Lebesgue measure on the Reals) are not a subset of the measurable functions. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑆 = dom vol    &   ⊢ (𝜑 → 𝑋 ⊆ ℝ)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑆)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ 0)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 ∈ (SMblFn‘𝑆) ∧ ¬ 𝑓 ∈ MblFn))