issues
search
math-comp
/
analysis
Mathematical Components compliant Analysis Library
Other
200
stars
44
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
subtypes and continuous functions
#1340
zstone1
opened
22 hours ago
0
Splitting normedmodtype.v
#1339
mkerjean
opened
2 days ago
0
Splitting Topology part 3: Separation axioms
#1338
zstone1
opened
2 days ago
0
weaken expR_ge1Dx
#1337
affeldt-aist
closed
2 days ago
0
add this lemma to `classical_orders.v` when dropping support for MathComp < 2.3
#1336
affeldt-aist
opened
4 days ago
0
removing troublesome lemma
#1335
zstone1
closed
4 days ago
1
move `Require Import` to top of the file
#1334
affeldt-aist
opened
4 days ago
0
Broken in Coq CI
#1333
SkySkimmer
closed
4 days ago
6
add in_nearW
#1332
IshiguroYoshihiro
closed
5 days ago
0
completely regular spaces and locally compact implies uniform
#1331
zstone1
opened
6 days ago
0
fixes #1329 (`maxeMr`)
#1330
affeldt-aist
closed
5 days ago
0
`maxeMr`: can be generalized to large inequality
#1329
affeldt-aist
closed
5 days ago
1
corollary to Vitali's theorem
#1328
affeldt-aist
opened
1 week ago
0
generalize integral_setD_EFin
#1327
IshiguroYoshihiro
closed
5 days ago
0
changelog for version 1.4.0
#1326
affeldt-aist
closed
1 week ago
0
fixes #1038 & #1284
#1325
affeldt-aist
closed
1 week ago
0
separating filters
#1324
zstone1
closed
4 days ago
4
fixing discrete topologies
#1323
zstone1
opened
2 weeks ago
3
fixes
#1322
affeldt-aist
closed
2 weeks ago
0
lexical ordering over nats
#1321
zstone1
closed
5 days ago
5
Near message error
#1320
mkerjean
opened
2 weeks ago
2
variant of `measurable_fun_eqr`
#1319
affeldt-aist
opened
3 weeks ago
0
Order topology
#1318
zstone1
closed
2 weeks ago
5
missing lemma about `indic`
#1317
affeldt-aist
closed
2 weeks ago
0
Drop support for 8.18
#1316
zstone1
closed
3 weeks ago
1
split `lebesgue_measure.v`
#1315
affeldt-aist
opened
4 weeks ago
0
fixes #1313 and moves Egorov
#1314
affeldt-aist
closed
4 weeks ago
2
wrong documentation
#1313
affeldt-aist
closed
4 weeks ago
0
Unpointed topologies with no backwards compatibility
#1312
zstone1
closed
3 weeks ago
1
Fixes 20240906
#1311
affeldt-aist
closed
1 month ago
0
generalize definitions introduced with Banach-Steinhaus PR
#1310
affeldt-aist
opened
1 month ago
0
unneeded local notation
#1309
affeldt-aist
closed
1 month ago
0
numeric local notations not needed anymore
#1308
affeldt-aist
closed
1 month ago
0
should be moved to the classical subdir
#1307
affeldt-aist
closed
1 month ago
0
lemmas about measurable from PR prob_lang
#1306
affeldt-aist
closed
3 weeks ago
0
unused `Reserved Notations` in `topology.v`?
#1305
affeldt-aist
closed
1 month ago
0
Add lemmas on divergent sequences
#1304
Yosuke-Ito-345
closed
1 week ago
4
fixes #1301
#1303
affeldt-aist
closed
1 month ago
0
fixes #1299 (minor generalization)
#1302
affeldt-aist
closed
1 month ago
0
documentation of `\;` needs fixing
#1301
affeldt-aist
closed
1 month ago
0
Topological vector spaces
#1300
mkerjean
opened
1 month ago
3
generalize `ge0_integral_closed_ball`
#1299
affeldt-aist
closed
1 month ago
0
fixes #1297
#1298
affeldt-aist
closed
1 month ago
1
domain of function parameter can be genralized
#1297
affeldt-aist
closed
1 month ago
0
duplicate use of `entourage_refl`?
#1296
affeldt-aist
closed
1 month ago
0
Lemma -> Let in HB.builders
#1295
affeldt-aist
closed
1 month ago
0
change of variables by nondecreasing/nonincreasing function
#1294
IshiguroYoshihiro
opened
1 month ago
0
lemmas about Lebesgue's outer measure
#1293
affeldt-aist
closed
1 month ago
0
`opp_ ...`, `... _opp` -> `oppr_ ...`, `... _ oppr`?
#1292
IshiguroYoshihiro
opened
1 month ago
0
Add lemmas `not_near_inftyP` and `not_near_ninftyP` in `normedtype.v`
#1291
Yosuke-Ito-345
closed
1 month ago
7
Next