List view

factorize code about powerset sigma-algebras

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 1438

#1438 In math-comp/analysis;

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

minor generalization

Status: Merged (completed).

math-comp/analysisnumber 1433

#1433 In math-comp/analysis;

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

add lemma measurable_powRr

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 1434

#1434 In math-comp/analysis;

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

prod notation for ereal and 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 1418

#1418 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

instances for measures

Status: Merged (completed).

math-comp/analysisnumber 1419

#1419 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

gen fset lemma for partitions

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 1422

#1422 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

deprecate approximation and make its interface accessible

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 1421

#1421 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

generalize the return type of RVs

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 1420

#1420 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

convergence of a real function

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 1396

#1396 In math-comp/analysis;

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

various fixes

Status: Merged (completed).

math-comp/analysisnumber 1409

#1409 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

rename homotopy_theory/path.v

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

#1426 In math-comp/analysis;

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

should be maxe_pMr

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

Status: Closed (completed).

#1389 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

rename to preimage_itv_cy ?

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

Status: Closed (completed).

#1390 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

too specific lemma

Status: Closed (completed).

#1408 In math-comp/analysis;

· by affeldt-aist was closed on Dec 3, 2024

two files named path.v

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

Status: Closed (completed).

#1412 In math-comp/analysis;

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

Path conflict on theories/homotopy_theory/path.v with core ssreflect path.v

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

Status: Closed (completed).

#1425 In math-comp/analysis;

· by MSoegtropIMC was closed on Dec 4, 2024