A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas
above its position. This means the list is a topological order of the dependency graph.
An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|
| monge-boundedge-f-above-bound | proved | all subs proved
| converges-neg-converges,
monle-boundedle-converges,
limit-neg-limit,
monle-boundedle-f-below-bound,
monge-neg-monle,
boundedge-neg-boundedle,
|
| monge-boundedge-limit-above-bound | proved | all subs proved
| converges-neg-converges,
monle-boundedle-converges,
limit-neg-limit,
monge-neg-monle,
boundedge-neg-boundedle,
monle-boundedle-limit-below-bound,
|
| monle-boundedle-limit-below-bound | proved | all subs proved
| boundedle-def,
monle-limit-sup,
|
| monle-boundedle-f-below-bound | proved | all subs proved
| boundedle-def,
monle-limit-sup,
|
| monge-limit-inf | proved | all subs proved
| boundedle-def,
monle-boundedle-converges,
converges-neg-converges,
limit-neg-limit,
monle-limit-sup,
monge-neg-monle,
boundedge-neg-boundedle,
|
| monle-limit-sup | proved | all subs proved
| limit-unique,
monle-boundedle-converges,
limit-def,
monle-converges-sup,
|
| monge-boundedge-converges | proved | all subs proved
| converges-neg-converges,
monle-boundedle-converges,
monge-neg-monle,
boundedge-neg-boundedle,
|
| limit-neg-limit | proved | all subs proved
| convergesto-neg-convergesto,
limit-def,
limit-unique,
converges-def,
|
| converges-neg-converges | proved | all subs proved
| convergesto-neg-convergesto,
converges-def,
|
| monle-boundedle-converges | proved | all subs proved
| converges-def,
monle-converges-sup,
|
| monge-converges-inf | proved | all subs proved
| convergesto-def,
boundedle-def,
monle-converges-sup,
monge-neg-monle,
boundedge-neg-boundedle,
|
| monle-converges-sup | proved | all subs proved
| monle-def,
boundedle-def,
convergesto-def,
|
| limit-unique | proved | all subs proved
| convergesto-def,
|
| convergesto-neg-convergesto | proved | all subs proved
| convergesto-def,
|
| boundedge-neg-boundedle | proved | all subs proved
| boundedle-def,
boundedge-def,
|
| monge-neg-monle | proved | all subs proved
| monle-def,
monge-def,
|
| monge-def | axiom | | |
| limit-def | axiom | | |
| converges-def | axiom | | |
| boundedge-def | axiom | | |
| convergesto-def | axiom | | |
| monle-def | axiom | | |
| boundedle-def | axiom | | |