List view

Urysohn'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 900

#900 In math-comp/analysis;

· by zstone1 was closed on Aug 4, 2023

Smallest filter

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 915

#915 In math-comp/analysis;

· by zstone1 was closed on Jun 27, 2023

minor generalizations, additions, fixes

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

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 974

#974 In math-comp/analysis;

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

Zorn lemma for inclusion

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 978

#978 In math-comp/analysis;

· by affeldt-aist was closed on Jul 20, 2023

fixes #979 (my_ball_le from local lemme to Let)

Status: Merged (completed).

math-comp/analysisnumber 980

#980 In math-comp/analysis;

· by affeldt-aist was closed on Jul 18, 2023

powere_pos lemmas

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

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 969

#969 In math-comp/analysis;

· by affeldt-aist was closed on Jul 6, 2023

minor generalizations, renaming

Status: Merged (completed).

math-comp/analysisnumber 985

#985 In math-comp/analysis;

· by affeldt-aist was closed on Jul 28, 2023

fixes #988 (bigcup_bigcup)

Status: Merged (completed).

math-comp/analysisnumber 989

#989 In math-comp/analysis;

· by affeldt-aist was closed on Jul 29, 2023

closed_bigcup

Status: Merged (completed).

math-comp/analysisnumber 991

#991 In math-comp/analysis;

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

add measurable_minr

Status: Merged (completed).

math-comp/analysisnumber 953

#953 In math-comp/analysis;

· by affeldt-aist was closed on Jun 28, 2023

minor fixes and additions to exp.v

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 939

#939 In math-comp/analysis;

· by affeldt-aist was closed on Jun 29, 2023

fixes #960

Status: Merged (completed).

math-comp/analysisnumber 961

#961 In math-comp/analysis;

· by affeldt-aist was closed on Jun 28, 2023

naming of integralM

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

Status: Closed (completed).

#938 In math-comp/analysis;

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

nbhs_closedballP -> nbhs_closed_ballP

Status: Closed (completed).

#983 In math-comp/analysis;

· by affeldt-aist was closed on Jul 29, 2023

bigcup_bigcup naming

Status: Closed (completed).

#988 In math-comp/analysis;

· by affeldt-aist was closed on Jul 29, 2023

bigcup_set naming

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

Status: Closed (completed).

#994 In math-comp/analysis;

· by affeldt-aist was closed on Jul 29, 2023

nneseriesrM -> nneseriesZl

Status: Closed (completed).

#982 In math-comp/analysis;

· by affeldt-aist was closed on Jul 28, 2023

my_ball_le shouldn't be seen

Status: Closed (completed).

#979 In math-comp/analysis;

· by affeldt-aist was closed on Jul 18, 2023