Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Basic measure theory
Lebesgue measure on n-dimensional Real numbers
ioovonmbl
Metamath Proof Explorer
Description: 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)
Ref
Expression
Hypotheses
ioovonmbl.x
⊢ ( 𝜑 → 𝑋 ∈ Fin )
ioovonmbl.s
⊢ 𝑆 = dom ( voln ‘ 𝑋 )
ioovonmbl.a
⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ* )
ioovonmbl.b
⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ* )
Assertion
ioovonmbl
⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )
Proof
Step
Hyp
Ref
Expression
1
ioovonmbl.x
⊢ ( 𝜑 → 𝑋 ∈ Fin )
2
ioovonmbl.s
⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3
ioovonmbl.a
⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ* )
4
ioovonmbl.b
⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ* )
5
1 3 4
ioorrnopnxr
⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
6
1 2 5
opnvonmbl
⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) (,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )