Library Coquelicot.AutoDerive
Library Coquelicot.Compactness
- Compactness: there is a finite covering of opens
- Compactness: there is a covering based on a gauge function
- Specific instances of compactness for 1D and 2D spaces
Library Coquelicot.Complex
- The set of complex numbers
- C is a NormedModule
- C is a CompleteSpace
- Locally compat
- Limits
- Derivatives
Library Coquelicot.Continuity
Library Coquelicot.Coquelicot
- Main types
- Main classes
- Low-level concepts of topology
- Limits and continuity
- Derivability and differentiability
- Riemann integrals
- Series and power series
- Naming conventions
Library Coquelicot.Derive
- Linear functions
- Differentiability using filters
- Differentiability in 1 dimentional space
- Definitions on R
- Operations
- Mean value theorem
- Newton integration
- Extension
- Iterated differential
- Taylor-Lagrange formula
Library Coquelicot.Derive_2d
- Differentiability
- Operations
- Partial derivatives
- Schwarz theorem
- Iterated differential
- 2D Taylor-Lagrange inequality
Library Coquelicot.Equiv
Library Coquelicot.ElemFct
- Absolute value
- Inverse function
- Square root function
- Power function
- Exponential function
- Natural logarithm
- Unnormalized sinc
- ArcTan
Library Coquelicot.Hierarchy
- Filters
- Algebraic spaces
- Uniform spaces defined using balls
- Modules
- Extended Types
- The topology on natural numbers
- The topology on real numbers
- Topology on R²
- Some Topology on Rbar
- Some limits on real functions
Library Coquelicot.Iter
Library Coquelicot.KHInt
Library Coquelicot.Lim_seq
Library Coquelicot.Lub
Library Coquelicot.Markov
Library Coquelicot.PSeries
Library Coquelicot.Rbar
- Definitions
- Compatibility with real numbers
- Properties of order
- Properties of operations
- Rbar_min
- Rbar_abs
Library Coquelicot.Rcomplements
- This file describes basic missing facts about the standard library of reals and a few concerning ssreflect.seq. It also contains a definition of the sign function.
- Integers
- Rinv
- Rdiv
- Rmult
- Rminus
- Rplus
- Rmin and Rmax
- Rabs
- Req
- posreal
- The sign function
- ssreflect.seq
- Operations on the Riemann integral
- Natural logarithm
- Other
Library Coquelicot.RInt
- Definition of Riemann integral
- Specific Normed Modules
- The total function RInt
- Equivalence with standard library
Library Coquelicot.RInt_analysis
- Continuity
- Riemann integral and differentiability
- Parametric integrals
- Power series
- Integration by parts
Library Coquelicot.RInt_gen
Library Coquelicot.Seq_fct
Library Coquelicot.Series
Library Coquelicot.SF_seq
This page has been generated by coqdoc