2013-04-09 hoelzl 2013-04-09 remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-03-26 hoelzl 2013-03-26 rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26 hoelzl 2013-03-26 separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-22 hoelzl 2013-03-22 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22 hoelzl 2013-03-22 move connected to HOL image; used to show intermediate value theorem
2013-03-22 hoelzl 2013-03-22 move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
2013-03-22 hoelzl 2013-03-22 move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
2013-03-22 hoelzl 2013-03-22 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2013-03-22 hoelzl 2013-03-22 move first_countable_topology to the HOL image
2013-03-22 hoelzl 2013-03-22 move metric_space to its own theory
2013-03-22 hoelzl 2013-03-22 move topological_space to its own theory
2013-03-06 hoelzl 2013-03-06 netlimit is abbreviation for Lim
2013-03-06 hoelzl 2013-03-06 tuned proofs
2013-03-06 hoelzl 2013-03-06 changed continuous_on_intros into a named theorems collection
2013-03-06 hoelzl 2013-03-06 changed continuous_intros into a named theorems collection
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2013-03-05 hoelzl 2013-03-05 eventually nhds represented using sequentially
2013-03-05 hoelzl 2013-03-05 generalized compact_Times to topological_space
2013-03-05 hoelzl 2013-03-05 move lemma Inf to usage point
2013-03-05 hoelzl 2013-03-05 tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
2013-03-05 hoelzl 2013-03-05 tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
2013-03-05 hoelzl 2013-03-05 generalized continuous/compact_attains_inf/sup from real to linorder_topology
2013-03-05 hoelzl 2013-03-05 continuity of pair operations
2013-03-05 hoelzl 2013-03-05 use generate_topology for second countable topologies, does not require intersection stable basis
2013-03-05 hoelzl 2013-03-05 generalized isGlb_unique
2013-02-13 immler 2013-02-13 eliminated union_closed_basis; cleanup Fin_Map
2013-02-13 immler 2013-02-13 fine grained instantiations
2013-02-13 immler 2013-02-13 generalized
2013-02-13 immler 2013-02-13 generalized
2013-01-31 hoelzl 2013-01-31 simplify heine_borel type class
2013-01-18 hoelzl 2013-01-18 generalized diameter from real_normed_vector to metric_space
2013-01-18 hoelzl 2013-01-18 tuned proof
2013-01-18 hoelzl 2013-01-18 tune prove compact_eq_totally_bounded
2013-01-17 huffman 2013-01-17 generalized theorem edelstein_fix to class metric_space
2013-01-17 huffman 2013-01-17 simplify proof of compact_imp_bounded
2013-01-15 huffman 2013-01-15 generalize more topology lemmas
2013-01-15 huffman 2013-01-15 generalize topology lemmas; simplify proofs
2013-01-17 hoelzl 2013-01-17 simplified prove of compact_imp_bounded
2013-01-17 hoelzl 2013-01-17 use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
2013-01-17 hoelzl 2013-01-17 move auxiliary lemma to top
2013-01-17 hoelzl 2013-01-17 add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite
2013-01-17 hoelzl 2013-01-17 group compactness-eq-seq-compactness lemmas together
2013-01-17 hoelzl 2013-01-17 replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
2013-01-17 hoelzl 2013-01-17 tuned
2013-01-17 hoelzl 2013-01-17 removed subseq_bigger (replaced by seq_suble)
2013-01-17 hoelzl 2013-01-17 countablility of finite subsets and rational numbers
2013-01-15 huffman 2013-01-15 generalized more topology theorems
2013-01-14 huffman 2013-01-14 generalize lemma islimpt_finite to class t1_space
2013-01-14 hoelzl 2013-01-14 differentiate (cover) compactness and sequential compactness
2013-01-14 hoelzl 2013-01-14 introduce first_countable_topology typeclass
2013-01-14 hoelzl 2013-01-14 move prod instantiation of second_countable_topology to its definition
2013-01-14 hoelzl 2013-01-14 renamed countable_basis_space to second_countable_topology
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-03 hoelzl 2012-12-03 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-16 hoelzl 2012-11-16 moved (b)choice_iff(') to Hilbert_Choice
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-16 immler 2012-11-16 allow arbitrary enumerations of basis in locale for generation of borel sets
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.