[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
,
Theorem base summary for Specification contfun-lim
Status:
Proved!
Axioms: 32, User Theorems: 18 (Proved: 18, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 1336, Interactions: 686
cont-def(0,0)
conttr-relative-def(0,0)
lift-not-trp-fininf(0,0)
lifted-def(0,0)
mon-relative-def(0,0)
montrl-equiv(36,21)
pconttr-lifted(96,53)
twomon-limsize(54,30)
cont-rel-thm(23,11)
conttr-relative-thm(237,121)
lift-not-trp-inffin(0,0)
liftedtr-def(0,0)
monl-def(0,0)
montrl-relative-def(0,0)
pdfclosedtr-def(0,0)
cont-relative-def(0,0)
conttr-thm(219,114)
lift-pcont(55,27)
lifttr-cont(62,32)
monl-equiv(24,15)
pbd-def(0,0)
pdfclosedtrl-def(0,0)
cont-relative-thm(133,60)
fun-neq(8,5)
lift-pred-fin(0,0)
lifttr-fin(0,0)
monl-relative-def(0,0)
pbd-relative-def(0,0)
pfxclosed-def(0,0)
cont-thm(106,53)
lift-cont(45,23)
lift-pred-inf(0,0)
lifttr-inf(0,0)
montr-def(0,0)
pbdtr-def(0,0)
pfxclosed-lift(18,8)
conttr-def(0,0)
lift-fin(0,0)
lift-trp-fin(0,0)
lifttr-pcont(74,41)
montr-relative-def(0,0)
pbdtr-relative-def(0,0)
pfxclosed-lift-tr(33,16)
conttr-rel-thm(39,18)
lift-inf(0,0)
lift-trp-inf(0,0)
mon-def(0,0)
montrl-def(0,0)
pcont-lifted(74,38)
pfxclosedl-def(0,0)