|
***
*** top (20:38:56 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
***
Proof summary for theory top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory top_basic
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory topology_prelim
discrete_topology_lem.................proved - complete [shostak](0.08 s)
indiscrete_topology_lem...............proved - complete [shostak](0.08 s)
topology_TCC1.........................proved - complete [shostak](0.02 s)
indiscrete_topology_TCC1..............proved - complete [shostak](0.02 s)
T0_topology_TCC1......................proved - complete [shostak](0.06 s)
T1_topology_TCC1......................proved - complete [shostak](0.06 s)
T2_topology_TCC1......................proved - complete [shostak](0.08 s)
hausdorff_TCC1........................proved - complete [shostak](0.02 s)
T0_is_topology........................proved - complete [shostak](0.03 s)
T1_is_T0..............................proved - complete [shostak](0.03 s)
T2_is_T1..............................proved - complete [shostak](0.05 s)
hausdorff_is_T2.......................proved - complete [shostak](0.02 s)
T2_is_hausdorff.......................proved - complete [shostak](0.02 s)
compact_space_TCC1....................proved - complete [shostak](0.12 s)
compact_space_is_topology.............proved - complete [shostak](0.02 s)
compact_hausdorff_is_topology.........proved - complete [shostak](0.10 s)
compact_hausdorff_is_hausdorff........proved - complete [shostak](0.10 s)
compact_hausdorff_is_compact_space....proved - complete [shostak](0.11 s)
connected_space_TCC1..................proved - complete [shostak](0.03 s)
connected_space_is_topology...........proved - complete [shostak](0.03 s)
Theory totals: 20 formulas, 20 attempted, 20 succeeded (1.10 s)
Proof summary for theory basis
synthetic_generated_def...............proved - complete [shostak](0.03 s)
synthetic_generated_alt_def...........proved - complete [shostak](0.08 s)
synthetic_generated_empty.............proved - complete [shostak](0.04 s)
synthetic_generated_full..............proved - complete [shostak](0.02 s)
synthetic_generated_Union.............proved - complete [shostak](0.10 s)
synthetic_generated_intersection......proved - complete [shostak](0.17 s)
synthetic_generated_topology_TCC1.....proved - complete [shostak](0.03 s)
synthetic_basis_is_topology...........proved - complete [shostak](0.02 s)
base_is_synthetic_base................proved - complete [shostak](0.06 s)
synthetic_base_is_base................proved - complete [shostak](0.04 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.58 s)
Proof summary for theory topology_def
second_countable_is_topology..........proved - complete [shostak](0.10 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.10 s)
Proof summary for theory topology
open_set_TCC1.........................proved - complete [shostak](0.03 s)
closed_set_TCC1.......................proved - complete [shostak](0.03 s)
clopen_set_TCC1.......................proved - complete [shostak](0.02 s)
compact_TCC1..........................proved - complete [shostak](0.04 s)
clopen_set_is_open....................proved - complete [shostak](0.03 s)
clopen_set_is_closed..................proved - complete [shostak](0.02 s)
open_complement.......................proved - complete [shostak](0.03 s)
closed_complement.....................proved - complete [shostak](0.03 s)
open_emptyset.........................proved - complete [shostak](0.03 s)
open_fullset..........................proved - complete [shostak](0.02 s)
open_Union............................proved - complete [shostak](0.04 s)
open_union............................proved - complete [shostak](0.08 s)
open_intersection.....................proved - complete [shostak](0.03 s)
open_Intersection.....................proved - complete [shostak](0.04 s)
closed_emptyset.......................proved - complete [shostak](0.03 s)
closed_fullset........................proved - complete [shostak](0.03 s)
closed_Intersection...................proved - complete [shostak](0.04 s)
closed_intersection...................proved - complete [shostak](0.05 s)
closed_union..........................proved - complete [shostak](0.05 s)
closed_Union..........................proved - complete [shostak](0.05 s)
complement_open_is_closed.............proved - complete [shostak](0.03 s)
complement_closed_is_open.............proved - complete [shostak](0.06 s)
emptyset_is_open......................proved - complete [shostak](0.02 s)
fullset_is_open.......................proved - complete [shostak](0.02 s)
union_is_open.........................proved - complete [shostak](0.03 s)
intersection_is_open..................proved - complete [shostak](0.04 s)
emptyset_is_closed....................proved - complete [shostak](0.04 s)
fullset_is_closed.....................proved - complete [shostak](0.04 s)
union_is_closed.......................proved - complete [shostak](0.05 s)
intersection_is_closed................proved - complete [shostak](0.06 s)
emptyset_is_clopen....................proved - complete [shostak](0.06 s)
fullset_is_clopen.....................proved - complete [shostak](0.06 s)
indiscrete_subset.....................proved - complete [shostak](0.08 s)
discrete_subset.......................proved - complete [shostak](0.08 s)
open_def..............................proved - complete [shostak](0.12 s)
neighbourhood_intersection............proved - complete [shostak](0.09 s)
neighbourhood_subset..................proved - complete [shostak](0.08 s)
Cl_split1.............................proved - complete [shostak](0.10 s)
Cl_split2.............................proved - complete [shostak](0.07 s)
subset_of_Cl..........................proved - complete [shostak](0.09 s)
Cl_subset.............................proved - complete [shostak](0.09 s)
Cl_idempotent.........................proved - complete [shostak](0.15 s)
eq_Cl_is_closed.......................proved - complete [shostak](0.14 s)
Cl_closed.............................proved - complete [shostak](0.07 s)
Cl_subset_closed......................proved - complete [shostak](0.07 s)
Cl_union..............................proved - complete [shostak](0.20 s)
Cl_Union..............................proved - complete [shostak](0.30 s)
Cl_Intersection.......................proved - complete [shostak](0.11 s)
open_difference.......................proved - complete [shostak](0.07 s)
closed_difference.....................proved - complete [shostak](0.08 s)
Cl_is_closed..........................proved - complete [shostak](0.06 s)
open_diff_closed_is_open..............proved - complete [shostak](0.07 s)
closed_diff_open_is_closed............proved - complete [shostak](0.06 s)
emptyset_is_compact...................proved - complete [shostak](0.06 s)
singleton_is_compact..................proved - complete [shostak](0.11 s)
union_is_compact......................proved - complete [shostak](0.17 s)
finite_is_compact.....................proved - complete [shostak](0.19 s)
compact_Union.........................proved - complete [shostak](-.55 s)
compact_def...........................proved - complete [shostak](0.33 s)
Theory totals: 59 formulas, 59 attempted, 59 succeeded (3.70 s)
Proof summary for theory prelude_sets_aux
complement_difference.................proved - complete [shostak](0.03 s)
Intersection_member...................proved - complete [shostak](0.03 s)
Intersection_split....................proved - complete [shostak](0.07 s)
Intersection_finite...................proved - complete [shostak](0.18 s)
Union_member..........................proved - complete [shostak](0.02 s)
Union_split...........................proved - complete [shostak](0.08 s)
Union_finite..........................proved - complete [shostak](0.10 s)
finite_Complement.....................proved - complete [shostak](0.09 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.60 s)
Proof summary for theory subspace
induced_subspace_topology.............proved - complete [shostak](0.27 s)
subspace_is_topology..................proved - complete [shostak](0.02 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.29 s)
Proof summary for theory lindelof
lindelof..............................proved - complete [shostak](0.32 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.32 s)
Proof summary for theory cross_product
cross_product_empty1..................proved - complete [shostak](0.02 s)
cross_product_empty2..................proved - complete [shostak](0.03 s)
cross_product_emptyset1...............proved - complete [shostak](0.03 s)
cross_product_emptyset2...............proved - complete [shostak](0.02 s)
cross_product_fullset.................proved - complete [shostak](0.02 s)
projection_product1...................proved - complete [shostak](0.04 s)
projection_product2...................proved - complete [shostak](0.04 s)
projection_1_emptyset.................proved - complete [shostak](0.02 s)
projection_2_emptyset.................proved - complete [shostak](0.03 s)
projection_1_fullset..................proved - complete [shostak](0.02 s)
projection_2_fullset..................proved - complete [shostak](0.03 s)
cross_product_empty1_rew..............proved - complete [shostak](0.02 s)
cross_product_empty2_rew..............proved - complete [shostak](0.03 s)
cross_product_full_rew................proved - complete [shostak](0.03 s)
cross_product_TCC1....................proved - complete [shostak](0.03 s)
product_projection....................proved - complete [shostak](0.06 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.47 s)
Proof summary for theory top_continuity
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory continuity_def
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory continuity
continuous_open_sets..................proved - complete [shostak](0.09 s)
continuous_closed_sets................proved - complete [shostak](0.05 s)
continuous_basis......................proved - complete [shostak](0.11 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.25 s)
Proof summary for theory continuity_subspace
subspace_continuous_at................proved - complete [shostak](0.11 s)
subspace_continuous...................proved - complete [shostak](0.03 s)
restrict_is_continuous................proved - complete [shostak](0.03 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.18 s)
Proof summary for theory constant_continuity
const_continuous_at...................proved - complete [shostak](0.08 s)
const_continuous......................proved - complete [shostak](0.03 s)
const_is_continuous...................proved - complete [shostak](0.04 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.15 s)
Proof summary for theory identity_continuity
id_continuous_at......................proved - complete [shostak](0.05 s)
id_continuous.........................proved - complete [shostak](0.02 s)
I_is_continuous.......................proved - complete [shostak](0.08 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.15 s)
Proof summary for theory composition_continuity
composition_continuous_at.............proved - complete [shostak](0.08 s)
composition_continuous................proved - complete [shostak](0.03 s)
composition_is_continuous.............proved - complete [shostak](0.03 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.15 s)
Proof summary for theory top_homeomorphic
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory homeomorphism_def
homeomorphism?_TCC1...................proved - complete [shostak](0.02 s)
homeomorphism_def.....................proved - complete [shostak](0.26 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.28 s)
Proof summary for theory homeomorphic_reflexive
homeomorphic_reflexive................proved - complete [shostak](0.10 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.10 s)
Proof summary for theory homeomorphic_symmetric
homeomorphic_symmetric................proved - complete [shostak](0.11 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.11 s)
Proof summary for theory homeomorphic_transitive
homeomorphic_transitive...............proved - complete [shostak](0.14 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.14 s)
Proof summary for theory top_convergence
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory topological_convergence
limit_TCC1............................proved - complete [shostak](0.56 s)
limit_lemma...........................proved - complete [shostak](0.03 s)
limit_accumulation....................proved - complete [shostak](0.10 s)
convergence_subsequence...............proved - complete [shostak](0.07 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.76 s)
Proof summary for theory subseq
subseq_index..........................proved - complete [shostak](0.04 s)
reflexive_subseq......................proved - complete [shostak](0.03 s)
transitive_subseq.....................proved - complete [shostak](0.05 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.13 s)
Proof summary for theory hausdorff_convergence
unique_limit..........................proved - complete [shostak](0.18 s)
limit_def.............................proved - complete [shostak](0.03 s)
singleton_is_closed...................proved - complete [shostak](0.13 s)
compact_is_closed.....................proved - complete [shostak](0.61 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.94 s)
Proof summary for theory top_connected
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory connected_def
connected_def.........................proved - complete [shostak](0.21 s)
connected_def2........................proved - complete [shostak](0.49 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.70 s)
Proof summary for theory connected_space
clopen_def............................proved - complete [shostak](0.05 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s)
Proof summary for theory top_compact
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory compact_spaces
compact_closed_def....................proved - complete [shostak](0.07 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.07 s)
Grand Totals: 152 proofs, 152 attempted, 152 succeeded (11.31 s)
[ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
]
|
