A formalization of properties of continuous functions on closed intervals

DOI10.1007/978-3-030-52200-1_27MaRDI QIDQ5041063zbMATH OpenOpenAlexFDO

Authors 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

closed intervalscontinuous functionsCoqformalizationlimits

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2003153
• Formalization of the integral calculus in the PVS theorem prover
• Formalization of real analysis: a survey of proof assistants and libraries
• Unified Proofs of Three Fundamental Properties of Continuous Functions
• An interactive calculus theorem-prover for continuity properties

Cites work

• A machine-checked proof of the odd order theorem
• Bolzano and uniform continuity
• Coquelicot: a user-friendly library of real analysis for Coq
• Formal proof
• Formal proof - the four color theorem
• Formal proof -- theory and practice
• scientific article; zbMATH DE number 3624817 (Why is no real title available?)
• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• scientific article; zbMATH DE number 2133322 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• scientific article; zbMATH DE number 5486212 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Who Gave You the Epsilon? Cauchy and the Origins of Rigorous Calculus

Cited in

(5)

• Formalization of the integral calculus in the PVS theorem prover
• scientific article; zbMATH DE number 2003153 (Why is no real title available?)
• Now f is continuous (exercise!)
• Unified Proofs of Three Fundamental Properties of Continuous Functions
• Fourier series formalization in ACL2(r)

Describes a project that uses

Uses Software

• Automath
• Coquelicot
• Coq

This page was built for publication: A formalization of properties of continuous functions on closed intervals

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5041063)