A Formalization of Properties of Continuous Functions on Closed Intervals

DOI10.1007/978-3-030-52200-1_27zbMath1503.68298OpenAlexW3041384201MaRDI QIDQ5041063

Yaoshun Fu, Wensheng Yu

Publication date: 13 October 2022

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-52200-1_27

zbMATH Keywords

limitscontinuous functionsCoqclosed intervalsformalization

Mathematics Subject Classification ID

Continuity and related questions (modulus of continuity, semicontinuity, discontinuities, etc.) for real functions in one variable (26A15) Mechanization of proofs and logical operations (03B35) Foundations: limits and generalizations, elementary topology of the line (26A03) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Automath
• Coquelicot

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Coquelicot: a user-friendly library of real analysis for Coq
• Bolzano and uniform continuity
• Who Gave You the Epsilon? Cauchy and the Origins of Rigorous Calculus
• A Machine-Checked Proof of the Odd Order Theorem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Formalization of Properties of Continuous Functions on Closed Intervals