List view

change of variables by nondecreasing/nonincreasing function

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

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

Status: Merged (completed).

math-comp/analysisnumber 1294

#1294 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Oct 8, 2024

generalize lime_sup_ge0

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 1252

#1252 In math-comp/analysis;

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

weaken expR_ge1Dx

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 1337

#1337 In math-comp/analysis;

· by affeldt-aist was closed on Oct 4, 2024

minor gen and addition

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 1341

#1341 In math-comp/analysis;

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

corollary to Vitali's theorem

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 1328

#1328 In math-comp/analysis;

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

Broken in Coq CI

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

Status: Closed (completed).

#1333 In math-comp/analysis;

· by SkySkimmer was closed on Oct 2, 2024

move Require Import to top of the file

Status: Closed (completed).

#1334 In math-comp/analysis;

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

duplicate line

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

Status: Closed (completed).

#1343 In math-comp/analysis;

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

\oo should be documented in filter.v

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

Status: Closed (completed).

#1342 In math-comp/analysis;

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

maxeMr: can be generalized to large inequality

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

#1329 In math-comp/analysis;

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