[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification contfun-lim

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:
lift-contprovedall subs proved pbd-def, monl-equiv, lift-inf, monl-def, lift-fin, mon-def, cont-def,
cont-rel-thmprovedall subs proved lift-pred-inf, pfxclosed-def, pfxclosedl-def, lift-pred-fin, mon-relative-def, cont-relative-def, cont-relative-thm,
lifttr-contprovedall subs proved pbdtr-def, montrl-equiv, lifttr-inf, montrl-def, lifttr-fin, montr-def, conttr-def,
conttr-rel-thmprovedall subs proved lift-trp-inf, pdfclosedtrl-def, pdfclosedtr-def, lift-trp-fin, conttr-relative-thm, montr-relative-def, conttr-relative-def,
conttr-relative-thmprovedall subs proved fun-neq, pdfclosedtr-def, pbdtr-relative-def, montr-relative-def, conttr-relative-def, twomon-limsize,
montrl-equivprovedall subs proved montrl-def,
cont-relative-thmprovedall subs proved fun-neq, pfxclosed-def, pbd-relative-def, mon-relative-def, cont-relative-def,
monl-equivprovedall subs proved monl-def,
pfxclosed-liftprovedall subs proved lift-pred-inf, lift-pred-fin, pfxclosedl-def, pfxclosed-def,
lifttr-pcontprovedall subs proved pbdtr-relative-def, lifttr-inf, lift-trp-inf, lifttr-fin, lift-trp-fin, montr-relative-def, conttr-relative-def, montrl-relative-def,
conttr-thmprovedall subs proved fun-neq, pbdtr-def, montr-def, conttr-def, twomon-limsize,
cont-thmprovedall subs proved fun-neq, pbd-def, mon-def, cont-def,
pcont-liftedprovedall subs proved pbd-relative-def, lift-pred-inf, lift-inf, lift-pred-fin, lift-fin, mon-relative-def, cont-relative-def, lifted-def, monl-relative-def,
lift-pcontprovedall subs proved pbd-relative-def, lift-inf, lift-pred-inf, lift-fin, lift-pred-fin, mon-relative-def, cont-relative-def, monl-relative-def,
pfxclosed-lift-trprovedall subs proved lift-trp-inf, lift-trp-fin, pdfclosedtr-def, pdfclosedtrl-def,
pconttr-liftedprovedall subs proved pbdtr-relative-def, lift-trp-inf, lifttr-inf, lift-trp-fin, lifttr-fin, montr-relative-def, conttr-relative-def, liftedtr-def, montrl-relative-def,
liftedtr-defaxiom
pdfclosedtrl-defaxiom
pdfclosedtr-defaxiom
monl-relative-defaxiom
lifted-defaxiom
pbd-relative-defaxiom
cont-relative-defaxiom
mon-relative-defaxiom
twomon-limsizeprovedall subs proved
conttr-defaxiom
montr-defaxiom
pbdtr-defaxiom
fun-neqprovedall subs proved
montrl-relative-defaxiom
conttr-relative-defaxiom
montr-relative-defaxiom
lift-trp-finaxiom
lifttr-finaxiom
lift-trp-infaxiom
lifttr-infaxiom
pbdtr-relative-defaxiom
cont-defaxiom
mon-defaxiom
lift-finaxiom
monl-defaxiom
lift-infaxiom
pbd-defaxiom
pfxclosed-defaxiom
pfxclosedl-defaxiom
lift-pred-finaxiom
lift-pred-infaxiom
montrl-defaxiom