List view

Alexandroff-Hausdorff Theorem and the Cantor Space

Status: Merged (completed).

math-comp/analysisnumber 834

#834 In math-comp/analysis;

· by zstone1 was closed on Nov 14, 2023

minimal changes to documentation to test coq2html

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

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

Status: Merged (completed).

math-comp/analysisnumber 1108

#1108 In math-comp/analysis;

· by affeldt-aist was closed on Jan 8, 2024

ae_eq lemmas

Status: Merged (completed).

math-comp/analysisnumber 1110

#1110 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Dec 21, 2023

Radon-Nikodym chain rule

Status: Merged (completed).

math-comp/analysisnumber 1083

#1083 In math-comp/analysis;

· by affeldt-aist was closed on Jan 6, 2024

cvg lemmas for fun

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

Status: Merged (completed).

math-comp/analysisnumber 1101

#1101 In math-comp/analysis;

· by affeldt-aist was closed on Dec 5, 2023

isolate the theory of lime_sup

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

Status: Merged (completed).

math-comp/analysisnumber 1121

#1121 In math-comp/analysis;

· by affeldt-aist was closed on Jan 7, 2024

restrain the scope of measurable args

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

Status: Merged (completed).

math-comp/analysisnumber 1116

#1116 In math-comp/analysis;

· by affeldt-aist was closed on Jan 7, 2024

Fixes 20231117

Status: Merged (completed).

math-comp/analysisnumber 1106

#1106 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

fixes #1123 (unusable lemma)

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

Status: Merged (completed).

math-comp/analysisnumber 1124

#1124 In math-comp/analysis;

· by affeldt-aist was closed on Dec 26, 2023

fixes #667

Status: Merged (completed).

math-comp/analysisnumber 1127

#1127 In math-comp/analysis;

· by affeldt-aist was closed on Dec 27, 2023

Hardy littlewood

Status: Merged (completed).

math-comp/analysisnumber 995

#995 In math-comp/analysis;

· by affeldt-aist was closed on Dec 14, 2023

Adds measurable_expR and measurable function composition

Status: Closed (abandoned).

math-comp/analysisnumber 1061

#1061 In math-comp/analysis;

· by hoheinzollern was closed on Dec 26, 2023

rm dup lemmas

Status: Merged (completed).

math-comp/analysisnumber 1129

#1129 In math-comp/analysis;

· by affeldt-aist was closed on Jan 1, 2024

helper lemmas for contra (PR #1119)

Status: Merged (completed).

math-comp/analysisnumber 1136

#1136 In math-comp/analysis;

· by Tragicus was closed on Jan 8, 2024

format doc

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

Status: Merged (completed).

math-comp/analysisnumber 1130

#1130 In math-comp/analysis;

· by affeldt-aist was closed on Jan 7, 2024

change contra_not when requiring MathComp > 1.14

Status: Closed (completed).

#667 In math-comp/analysis;

· by affeldt-aist was closed on Dec 27, 2023

non-informative comment

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

Status: Closed (completed).

#1104 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

lacks a Proof command

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

Status: Closed (completed).

#1103 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

Lacking a Proof command

Status: Closed (completed).

#1114 In math-comp/analysis;

· by affeldt-aist was closed on Jan 8, 2024

unsusable lemma

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

Status: Closed (completed).

#1123 In math-comp/analysis;

· by affeldt-aist was closed on Dec 26, 2023

coqdoc formatting command

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

Status: Closed (completed).

#1071 In math-comp/analysis;

· by affeldt-aist was closed on Jan 8, 2024

Alternative definition of Chernoff

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: Closed (completed).

#1078 In math-comp/analysis;

· by hoheinzollern was closed on Jan 8, 2024

Add cantor.v to theories/Make

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

Status: Closed (completed).

#1098 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

Is cantor_pseudoMetric necessary?

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

Status: Closed (completed).

#1099 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

move ae_eq?

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

Status: Closed (completed).

#1096 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Dec 21, 2023