Formal Analysis in Coq
(********************************)
Foundations_of_Analysis -- A formalization of Landau's "Foundations of Analysis".
Pre_Logic.v (Preparatory logic)
Pre_Ensemble.v (Preliminary knowledge of set theory)
Nats.v (Natural numbers)
frac.v (Fractions)
cuts.v (Cuts)
reals.v (Real numbers)
DFT.v (Dedekind fundamental theorem)
complex.v (Complex numbers)
(++++++++++++++++++++++++++)
extension -- A formalization of extension for real numbers.
finite.v (Finiteness related content)
R_sup.v (Supplement for real numbers)
R_sup1.v (Another supplement for real numbers)
Seq.v (Sequence related content)
(++++++++++++++++++++++++++)
Properties_of_continuous_functions_on_closed_intervals -- A formalization of properties of continuous functions on closed intervals.
fun.v (A formalization of properties of continuous functions on closed intervals)
(++++++++++++++++++++++++++)
completeness -- A formalization of cyclic proof of real number completeness theorem.
t1.v (Dedekind fundamental theorem prove Supremum theorem)
t1_1.v (Supremum theorem prove Dedekind fundamental theorem)
t2.v (Supremum theorem prove Monotone convergence theorem)
t3.v (Monotone convergence theorem prove Nested interval theorem)
t4.v (Nested interval theorem prove Finite cover theorem)
t5.v (Finite cover theorem prove Accumulation point theorem)
t6.v (Accumulation point theorem prove Sequential compactness theorem)
t7.v (Sequential compactness theorem prove Cauchy completeness theorem)
t8.v (Cauchy completeness theorem prove Dedekind fundamental theorem)
(++++++++++++++++++++++++++)
Calculus_without_limt -- A formalization of calculus without limit theory.
calpre.v (Preliminary knowledge of this theory)
DCF.v (Difference-Quotient Control Function)
UnD.v (Uniform Derivative)
StD.v (Strong Derivative)
IntSys.v (Integral System and Definite Integral)
HighDer.v (Higher Order Derivative)
calTh.v (Important Theorems in Calculus)
Hstd.v (Higher order strong derivative)
(++++++++++++++++++++++++++)
completeness_IVT -- A formalization of completeness of intermediate value theorem.
intsup.v (A formalization of completeness of intermediate value theorem)