List view

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: Open (in progress).

math-comp/analysisnumber 1589

#1589 In math-comp/analysis;

· affeldt-aist opened on Apr 24, 2025

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

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

Missing canonical declaration in topology.v?

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

Status: Open.

#154 In math-comp/analysis;

· amahboubi opened on Oct 4, 2019

renaming of <code>conv</code>

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

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

Status: Open.

#860 In math-comp/analysis;

· affeldt-aist opened on Feb 28, 2023

Generalize to <code>l : \bar R</code>?

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

Status: Open.

#1485 In math-comp/analysis;

· affeldt-aist opened on Feb 18, 2025

expectation of product

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 1391

#1391 In math-comp/analysis;

· affeldt-aist opened on Nov 13, 2024

generalize <code>cvg_nbhsP</code> in <code>realfun.v</code> to any metric space

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

Status: Open.

#1437 In math-comp/analysis;

· affeldt-aist opened on Dec 17, 2024

<code>conv_gt0</code> as an instance of <code>PosNum</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.

#1009 In math-comp/analysis;

· affeldt-aist opened on Aug 11, 2023

rm tests in<code>itv.v</code> (now <code>interval_inference.v</code>)

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

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

Status: Open.

#880 In math-comp/analysis;

· affeldt-aist opened on Mar 15, 2023

naming and definition of <code>monotonous</code>

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

Status: Open.

#1133 In math-comp/analysis;

· affeldt-aist opened on Jan 7, 2024

Could we have a nix upgrade documentation somewhere? (@amahboubi)

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

Status: Open.

#151 In math-comp/analysis;

· CohenCyril opened on Sep 17, 2019

potential generalization from <code>realDomainType</code> to <code>numDomainType</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.

#696 In math-comp/analysis;

· affeldt-aist opened on Jul 13, 2022

Generalize integration_by_parts

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

Status: Open (in progress).

math-comp/analysisnumber 1674

#1674 In math-comp/analysis;

· IshiguroYoshihiro opened on Jul 4, 2025

Normed vector types, infinite norm, norm equivalence thm, continuity …

Status: Open (in progress).

math-comp/analysisnumber 1718

#1718 In math-comp/analysis;

· Tragicus opened on Sep 16, 2025

Have a spec lemma for big0

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

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

Status: Open.

#102 In math-comp/analysis;

· CohenCyril opened on Sep 14, 2018

improve the interface for the product measure

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

Status: Open.

#1665 In math-comp/analysis;

· affeldt-aist opened on Jul 1, 2025

notation for <code>ae_eq</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.

#1079 In math-comp/analysis;

· affeldt-aist opened on Nov 2, 2023

Should poweR return 0 if the exponent is negative?

Status: Open.

#1401 In math-comp/analysis;

· jmmarulang opened on Nov 18, 2024

Fix 'the_* landau notation to improve readability

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

Status: Open.

#2 In math-comp/analysis;

· CohenCyril opened on Jan 11, 2018

Organization of the files in <code>lebesgue_integral_theory</code>

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

Status: Open.

#1549 In math-comp/analysis;

· affeldt-aist opened on Apr 2, 2025

<code>R^o</code> type constraints in <code>ln_concave</code>

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

help 🆘This author/reviewer of this issue/PR needs external helpThis author/reviewer of this issue/PR needs external help

Status: Open (in progress).

math-comp/analysisnumber 1010

#1010 In math-comp/analysis;

· affeldt-aist opened on Aug 11, 2023