A Coq Formalization of Lebesgue Integration of Nonnegative Functions

DOI10.1007/s10817-021-09612-0arXiv2104.05256MaRDI QIDQ6365053

Florian Faissole, Micaela Mayero, Vincent Martin, Sylvie Boldo, François Clément

Publication date: 12 April 2021

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

This page was built for publication: A Coq Formalization of Lebesgue Integration of Nonnegative Functions