Reconstruction of the one-dimensional Lebesgue measure

DOI10.2478/forma-2020-0008zbMath1462.68224OpenAlexW3033931426MaRDI QIDQ2658815

Noboru Endou

Publication date: 24 March 2021

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2020-0008

zbMATH Keywords

Lebesgue measurealgebra of intervals

Mathematics Subject Classification ID

Contents, measures, outer measures, capacities (28A12) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

Relationship between the Riemann and Lebesgue integrals ⋮ Measure construction by extension in dependent type theory with application to integration

Uses Software

• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Cartesian Products of Family of Real Linear Spaces
• Mizar: State-of-the-art and Beyond

This page was built for publication: Reconstruction of the one-dimensional Lebesgue measure