3 search results for "tag:"keyword:metric""

Showing 1 - 3
  1. coq-coquelicot

    No documentation

    A Coq formalization of real analysis compatible with the standard library
    keyword:real analysis keyword:topology keyword:filters keyword:metric spaces category:Mathematics/Real Calculus and Topology logpath:Coquelicot date:2025-01-27
    Sylvie Boldo <sylvie.boldo@inria.fr> Catherine Lelay <catherine.lelay@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>
    3.4.3
    LGPL-3.0-or-later
    Used by 7 other packages
    27 Jan 2025
  2. coq-hol-light

    No documentation

    HOL-Light library in Coq
    logpath:HOLLight date:2025-01-20 category:Math/Arith/Misc category:Math/Arith/Real Numbers category:Math/Real Numbers category:Mathematics/Real Calculus and Topology keyword:HOL-Light keyword:list keyword:basic set theory keyword:arithmetic keyword:integer keyword:real keyword:complex keyword:permutation keyword:group keyword:matroid keyword:binomial keyword:topology keyword:metric keyword:space keyword:analysis keyword:homology keyword:vector keyword:linear keyword:algebra keyword:convex keyword:path keyword:polytope keyword:Brouwer keyword:degree keyword:derivative keyword:Clifford keyword:integration keyword:measure keyword:Lebesgue keyword:transcendental
    Frédéric Blanqui
    3.0.0
    CeCILL-2.1
    Used by 0 other packages
    21 Jan 2025
  3. coq-topology

    No documentation

    General topology in Coq
    category:Mathematics/Real Calculus and Topology date:2023-08-18 keyword:topology keyword:filters keyword:nets keyword:metric spaces keyword:real analysis keyword:Urysohn's lemma keyword:Tietze extension theorem logpath:Topology
    Daniel Schepler
    10.2.0
    LGPL-2.1-or-later
    Used by 0 other packages
    21 Aug 2023