Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure

DOI10.1007/978-3-642-14052-5_4zbMath1291.68335OpenAlexW1514186392MaRDI QIDQ5747639

John Cowles, Ruben A. Gamboa

Publication date: 14 September 2010

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_4

Mathematics Subject Classification ID

Classes of sets (Borel fields, (sigma)-rings, etc.), measurable sets, Suslin sets, analytic sets (28A05)

Related Items (1)

Formalization of real analysis: a survey of proof assistants and libraries

Uses Software

• ACL2

This page was built for publication: Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure