List view

Lebesgue Stieltjes 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 677

#677 In math-comp/analysis;

· by affeldt-aist was closed on Oct 23, 2023

easy lemmas

Status: Merged (completed).

math-comp/analysisnumber 1090

#1090 In math-comp/analysis;

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

Fixes 20231108

Status: Merged (completed).

math-comp/analysisnumber 1081

#1081 In math-comp/analysis;

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

fixes #1052 (renaming in sequences.v)

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 1085

#1085 In math-comp/analysis;

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

tentative formalization of Vitali's 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 973

#973 In math-comp/analysis;

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

tentative formalization of 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 984

#984 In math-comp/analysis;

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

Minkowski

Status: Merged (completed).

math-comp/analysisnumber 1000

#1000 In math-comp/analysis;

· by hoheinzollern was closed on Nov 13, 2023

fixes #1049

Status: Merged (completed).

math-comp/analysisnumber 1050

#1050 In math-comp/analysis;

· by affeldt-aist was closed on Oct 10, 2023

fixes #1056

Status: Merged (completed).

math-comp/analysisnumber 1057

#1057 In math-comp/analysis;

· by affeldt-aist was closed on Oct 15, 2023

negligible_bigcup

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 1058

#1058 In math-comp/analysis;

· by affeldt-aist was closed on Oct 15, 2023

Fixes 1042, 1037, 1045, 1046

Status: Merged (completed).

math-comp/analysisnumber 1043

#1043 In math-comp/analysis;

· by affeldt-aist was closed on Oct 9, 2023

New notations of negative/positive_set

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 1062

#1062 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Oct 20, 2023

fixes #1051 (rename lim_sup -> limn_sup)

Status: Merged (completed).

math-comp/analysisnumber 1068

#1068 In math-comp/analysis;

· by affeldt-aist was closed on Oct 30, 2023

typo

Status: Closed (completed).

#1074 In math-comp/analysis;

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

lacking documentation

Status: Closed (completed).

#1064 In math-comp/analysis;

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

unused variable

Status: Closed (completed).

#1063 In math-comp/analysis;

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

ereal_nondecreasing_cvg -> ereal_nondecreasing_cvgn

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

Status: Closed (completed).

#1052 In math-comp/analysis;

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

spurious parameter

Status: Closed (completed).

#1054 In math-comp/analysis;

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

order of parameters

Status: Closed (completed).

#1055 In math-comp/analysis;

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

use the \d_ notation?

Status: Closed (completed).

#1056 In math-comp/analysis;

· by affeldt-aist was closed on Oct 15, 2023

lim_sup -> limn_sup

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

Status: Closed (completed).

#1051 In math-comp/analysis;

· by affeldt-aist was closed on Oct 30, 2023

cvg_at_rightE could be moved

Status: Closed (completed).

#1066 In math-comp/analysis;

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

ball_filter can be generalized

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

#1042 In math-comp/analysis;

· by affeldt-aist was closed on Oct 9, 2023

Lnorm should be locked

Status: Closed (completed).

#1037 In math-comp/analysis;

· by CohenCyril was closed on Oct 9, 2023

missing type class instance?

Status: Closed (completed).

#1049 In math-comp/analysis;

· by affeldt-aist was closed on Oct 10, 2023