List view

Banachsteinhaus

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 334

#334 In math-comp/analysis;

· by mkerjean was closed on Sep 5, 2024

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

math-comp/analysisnumber 1266

#1266 In math-comp/analysis;

· by affeldt-aist was closed on Sep 17, 2024

lemmas about measurable from PR prob_lang

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 1306

#1306 In math-comp/analysis;

· by affeldt-aist was closed on Sep 15, 2024

variants of existing lemmas

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 1288

#1288 In math-comp/analysis;

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

to avoid a universe inconsistency with ring

"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 1287

#1287 In math-comp/analysis;

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

Lemma -> Let in HB.builders

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 1295

#1295 In math-comp/analysis;

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

fixes #1297

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 1298

#1298 In math-comp/analysis;

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

lemmas about Lebesgue's outer 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 1293

#1293 In math-comp/analysis;

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

add 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 1285

#1285 In math-comp/analysis;

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

minor additions and generalizations

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 1289

#1289 In math-comp/analysis;

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

fixes #1299 (minor generalization)

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 1302

#1302 In math-comp/analysis;

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

fixes #1301

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 1303

#1303 In math-comp/analysis;

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

Unpointed topologies with no backwards compatibility

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 1312

#1312 In math-comp/analysis;

· by zstone1 was closed on Sep 13, 2024

fixes #1313 and moves Egorov

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 1314

#1314 In math-comp/analysis;

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

Drop support for 8.18

Status: Merged (completed).

math-comp/analysisnumber 1316

#1316 In math-comp/analysis;

· by zstone1 was closed on Sep 13, 2024

fixes #1038 & #1284

Status: Merged (completed).

math-comp/analysisnumber 1325

#1325 In math-comp/analysis;

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

fixes

Status: Merged (completed).

math-comp/analysisnumber 1322

#1322 In math-comp/analysis;

· by affeldt-aist was closed on Sep 21, 2024

domain of function parameter can be genralized

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).

#1297 In math-comp/analysis;

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

generalize ge0_integral_closed_ball

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).

#1299 In math-comp/analysis;

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

duplicate use of entourage_refl?

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

Status: Closed (completed).

#1296 In math-comp/analysis;

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

documentation of \; needs fixing

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

Status: Closed (completed).

#1301 In math-comp/analysis;

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

unused Reserved Notations in topology.v?

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

Status: Closed (completed).

#1305 In math-comp/analysis;

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

missing lemma about indic

Status: Closed (completed).

#1317 In math-comp/analysis;

· by affeldt-aist was closed on Sep 21, 2024

unneeded local notation

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

Status: Closed (completed).

#1309 In math-comp/analysis;

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

numeric local notations not needed anymore

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

Status: Closed (completed).

#1308 In math-comp/analysis;

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