List view

Wochoice

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 1198

#1198 In math-comp/analysis;

· by Tragicus was closed on Aug 6, 2024

identifier for completed lebesgue measure

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 1224

#1224 In math-comp/analysis;

· by affeldt-aist was closed on Jun 26, 2024

fixes #1126

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 1263

#1263 In math-comp/analysis;

· by affeldt-aist was closed on Jul 22, 2024

left/right lim prop for monotonic 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 1265

#1265 In math-comp/analysis;

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

add Coq 8.20

Status: Merged (completed).

math-comp/analysisnumber 1275

#1275 In math-comp/analysis;

· by affeldt-aist was closed on Jul 30, 2024

missing lemmas about ereal

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 1264

#1264 In math-comp/analysis;

· by affeldt-aist was closed on Jul 25, 2024

Lemma invf_ltp

Status: Merged (completed).

math-comp/analysisnumber 1267

#1267 In math-comp/analysis;

· by hoheinzollern was closed on Jul 30, 2024

setX -> setY; setM -> setX

Status: Merged (completed).

math-comp/analysisnumber 1276

#1276 In math-comp/analysis;

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

at_left version of an at_right lemma

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 1255

#1255 In math-comp/analysis;

· by affeldt-aist was closed on Jul 19, 2024

fixes #1241

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

Status: Merged (completed).

math-comp/analysisnumber 1242

#1242 In math-comp/analysis;

· by affeldt-aist was closed on Jun 20, 2024

fixes #1231 (space ball lemma)

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 1247

#1247 In math-comp/analysis;

· by affeldt-aist was closed on Jun 24, 2024

FTC1 corollary

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 1246

#1246 In math-comp/analysis;

· by affeldt-aist was closed on Jul 30, 2024

fixes #1248 (to_set / xsection)

Status: Merged (completed).

math-comp/analysisnumber 1249

#1249 In math-comp/analysis;

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

rename setD_closed to setSD_closed

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

Status: Merged (completed).

math-comp/analysisnumber 1243

#1243 In math-comp/analysis;

· by affeldt-aist was closed on Jul 22, 2024

fixes #330 (floor and ceil subsumed by MathComp)

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

Status: Merged (completed).

math-comp/analysisnumber 1244

#1244 In math-comp/analysis;

· by affeldt-aist was closed on Jul 16, 2024

fixes #1253 (redundant instantiation)

Status: Merged (completed).

math-comp/analysisnumber 1254

#1254 In math-comp/analysis;

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

new factory for algebra of sets

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 1251

#1251 In math-comp/analysis;

· by affeldt-aist was closed on Jul 31, 2024

floor and ceil to be subsumed by MathComp

Status: Closed (completed).

#330 In math-comp/analysis;

· by affeldt-aist was closed on Jul 16, 2024

Missing subspace lemma on balls

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

Status: Closed (completed).

#1231 In math-comp/analysis;

· by CohenCyril was closed on Jun 24, 2024

use patch here?

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

Status: Closed (completed).

#1100 In math-comp/analysis;

· by affeldt-aist was closed on Jul 30, 2024

better advertise the coq-mathcomp-classical

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

Status: Closed (completed).

#1126 In math-comp/analysis;

· by affeldt-aist was closed on Jul 22, 2024

update using MathComp 1.17.0 naming convention

Status: Closed (completed).

#1241 In math-comp/analysis;

· by affeldt-aist was closed on Jun 20, 2024

inf_lb should be inf_lbound?

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

Status: Closed (completed).

#1258 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Jul 30, 2024

duplicate section

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

Status: Closed (completed).

#1270 In math-comp/analysis;

· by affeldt-aist was closed on Jul 30, 2024

typo in measure.v

Status: Closed (completed).

#1277 In math-comp/analysis;

· by affeldt-aist was closed on Aug 2, 2024