Search results

naming is off in limit_point_infinite_setP

Status: Open.

#1930 In math-comp/analysis;

· affeldt-aist opened on Apr 4, 2026

continuous_linear_bounded should be generalized to convexTvsType

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

Status: Open.

#1927 In math-comp/analysis;

· affeldt-aist opened on Apr 3, 2026

·  

1.17.0

rename to continuous_fun?

Status: Open.

#1926 In math-comp/analysis;

· affeldt-aist opened on Apr 3, 2026

·  

1.17.0

rename sub_sigma_algebra2

Status: Open.

#1923 In math-comp/analysis;

· affeldt-aist opened on Mar 31, 2026

·  

1.17.0

move preimage_set_system to classical_sets.v?

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

Status: Open.

#1922 In math-comp/analysis;

· affeldt-aist opened on Mar 30, 2026

consider making the information r > 0 explicit in open_subball_rat?

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

Status: Open.

#1920 In math-comp/analysis;

· affeldt-aist opened on Mar 26, 2026

·  

1.17.0

setUitv1 and setU1itv

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

Status: Open.

#1914 In math-comp/analysis;

· affeldt-aist opened on Mar 20, 2026

·  

1.17.0

Vector space with basis

Status: Open.

#1911 In math-comp/analysis;

· Tragicus opened on Mar 19, 2026

packager: coq -> rocq

packaging/releasingIssue/PR about packaging or realising.Issue/PR about packaging or realising.

Status: Open.

#1905 In math-comp/analysis;

· affeldt-aist opened on Mar 16, 2026

·  

1.17.0

funrpos and funepos should be factorized

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

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

Status: Open.

#1903 In math-comp/analysis;

· affeldt-aist opened on Mar 15, 2026

·  

1.17.0

is_derive instances for max function

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

Status: Open.

#1898 In math-comp/analysis;

· affeldt-aist opened on Mar 12, 2026

·  

1.17.0

about the notation f \max g

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

Status: Open.

#1897 In math-comp/analysis;

· affeldt-aist opened on Mar 12, 2026

·  

1.17.0