Rob Lewis
|
2c56a2c48b
|
feat(theories/{analysis, topology}): show eps-delta and topological continuity coincide on metric spaces
|
2016-02-12 11:50:10 -08:00 |
|
Rob Lewis
|
685049988c
|
feat(theories/analysis): define metric topology
|
2016-02-12 11:50:10 -08:00 |
|
Rob Lewis
|
87ec5ada07
|
fix(analysis/metric_space): unnecessary import, style, remove unnecessary lines
|
2016-02-04 11:03:28 -08:00 |
|
Rob Lewis
|
f402f322aa
|
feat(theories/analysis): add theorems about convergent sequences, functions, and continuity
|
2016-02-04 11:03:28 -08:00 |
|
Rob Lewis
|
796e16bdb7
|
feat(library/theories/analysis): add theorems about convergent functions in metric spaces
|
2016-02-04 11:03:28 -08:00 |
|
Jeremy Avigad
|
86fc326e08
|
refactor/feat(library/theories/analysis/*): reorganize analysis library and add some theorems
|
2016-01-16 10:53:56 -08:00 |
|
Jeremy Avigad
|
84cdf3d36d
|
feat(library/theories/analysis/normed_space): start theory of normed spaces for analysis
|
2015-12-22 16:39:13 -05:00 |
|
Jeremy Avigad
|
08fbf127c6
|
feat(library/theories/analysis/metric_space,real_limit): define complete metric space, make real an instance
|
2015-12-22 16:39:13 -05:00 |
|
Leonardo de Moura
|
b94e31a72c
|
refactor(library): remove algebra namespace
|
2015-12-05 23:50:01 -08:00 |
|
Jeremy Avigad
|
2beb0030d6
|
refactor(library/*): protect sub in nat, div in nat and int
|
2015-11-08 14:04:59 -08:00 |
|
Leonardo de Moura
|
6df31d3406
|
refactor(library/data/nat/basic): mark some theorems as protected to avoid overloading
|
2015-11-08 14:04:56 -08:00 |
|
Leonardo de Moura
|
9fb59a05f5
|
fix(library/theories/analysis/metric_space): minor correction
|
2015-11-08 14:04:55 -08:00 |
|
Jeremy Avigad
|
42c9bdc463
|
feat(library/theories/analysis/{metric_space,real_limit}: add convergence theorems
|
2015-09-20 20:51:28 -04:00 |
|
Rob Lewis
|
d6be32e4ef
|
feat(library/theories/analysis): refactor IVT proof, add more general version of IVT
|
2015-09-17 16:22:46 -04:00 |
|
Rob Lewis
|
ea3915f279
|
feat(library/theories/analysis): prove intermediate value theorem
|
2015-09-16 08:28:11 -07:00 |
|
Jeremy Avigad
|
352a906ba2
|
feat(library/theories/{metric_space,real_limit}): define metric spaces, limits, instantiate reals
|
2015-09-12 21:46:09 -04:00 |
|