List view

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

Status: Open.

#1067 In math-comp/analysis;

· affeldt-aist opened on Oct 23, 2023

Sorgenfrey line

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1044 In math-comp/analysis;

· affeldt-aist opened on Oct 4, 2023

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

Fundamental Theorem of Calculus

Status: Open.

#965 In math-comp/analysis;

· zstone1 opened on Jun 27, 2023

variant of <code>measurable_fun_eqr</code>

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1319 In math-comp/analysis;

· affeldt-aist opened on Sep 15, 2024

metric structure

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

Status: Draft (not ready).

math-comp/analysisnumber 1589

#1589 In math-comp/analysis;

· affeldt-aist opened on Apr 24, 2025

improve the documentation of <code>contra.v</code>

documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repository

Status: Open.

#1197 In math-comp/analysis;

· affeldt-aist opened on Mar 28, 2024

finitely-supported probability measure

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1227 In math-comp/analysis;

· affeldt-aist opened on May 27, 2024

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

derive -&gt; differentiable

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#304 In math-comp/analysis;

· mkerjean opened on Dec 10, 2020

<code>semi_additive</code> is also defined in MathComp 2

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

Status: Open.

#1072 In math-comp/analysis;

· affeldt-aist opened on Oct 30, 2023

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

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

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

near notation inference issues

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Open.

#548 In math-comp/analysis;

· zstone1 opened on Feb 24, 2022

Put <code>iavg</code> in its own file

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

Status: Open.

#1555 In math-comp/analysis;

· affeldt-aist opened on Apr 2, 2025

notation for intervals

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

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

Status: Open.

#795 In math-comp/analysis;

· affeldt-aist opened on Nov 10, 2022

Solve slowdown in derive

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

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

Status: Open.

#118 In math-comp/analysis;

· CohenCyril opened on Oct 30, 2018

Redundancies between <code>realseq.v</code> and <code>sequences.v</code>

question ❓There is an unanswered question hereThere is an unanswered question here

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

Status: Open.

#255 In math-comp/analysis;

· affeldt-aist opened on Sep 4, 2020

Document the sub-directories of <code>theories</code>

documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repository

Status: Open.

#1550 In math-comp/analysis;

· affeldt-aist opened on Apr 2, 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

Near message error

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

question ❓There is an unanswered question hereThere is an unanswered question here

Status: Open.

#1320 In math-comp/analysis;

· mkerjean opened on Sep 16, 2024

Add closed sets to topological mixin

Status: Open.

#134 In math-comp/analysis;

· drouhling opened on Mar 1, 2019

Near Notation can't solve <code>g \is_near F</code>

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Open.

#549 In math-comp/analysis;

· zstone1 opened on Feb 24, 2022

candidate lemma for a PR (<code>bounded</code>, <code>lee_sum</code>, <code>nneseries</code>)

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1530 In math-comp/analysis;

· affeldt-aist opened on Mar 17, 2025