List view

WIP: eudoxus reals

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

TODO: MC2 portThis PR must be ported to mathcomp 2 now that the. Remove this label when the port is done.This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done.

Status: Draft (not ready).

math-comp/analysisnumber 116

#116 In math-comp/analysis;

· strub opened on Oct 17, 2018

naming in <code>classical_sets</code> conflicts with <code>fintype</code>

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#274 In math-comp/analysis;

· affeldt-aist opened on Nov 9, 2020

move dyadic intervals in a more appropriate file

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1553 In math-comp/analysis;

· affeldt-aist opened on Apr 2, 2025

put together statements about <code>]x-r,x+r[</code>

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1084 In math-comp/analysis;

· affeldt-aist opened on Nov 9, 2023

shorten proof about monotonic functions

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1156 In math-comp/analysis;

· affeldt-aist opened on Jan 18, 2024

Fundamental Theorem of Calculus

Status: Open.

#965 In math-comp/analysis;

· zstone1 opened on Jun 27, 2023

CPOs (wip)

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Draft (not ready).

math-comp/analysisnumber 1807

#1807 In math-comp/analysis;

· affeldt-aist opened on Dec 22, 2025

move the product measure out of <code>lebesgue_integral_fubini.v</code>

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1554 In math-comp/analysis;

· affeldt-aist opened on Apr 2, 2025

generalize <code>Order_isNbhs</code>

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1779 In math-comp/analysis;

· affeldt-aist opened on Nov 27, 2025

introduce a file <code>real_topology.v</code>

Status: Open.

#1067 In math-comp/analysis;

· affeldt-aist opened on Oct 23, 2023