src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
Sat, 25 May 2013 15:44:29 +0200 haftmann weaker precendence of syntax for big intersection and union on sets
Wed, 24 Apr 2013 13:28:30 +0200 hoelzl spell conditional_ly_-complete lattices correct
Tue, 09 Apr 2013 14:04:41 +0200 hoelzl remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
Tue, 26 Mar 2013 12:21:00 +0100 hoelzl rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
Tue, 26 Mar 2013 12:20:52 +0100 hoelzl separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move connected to HOL image; used to show intermediate value theorem
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl 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)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move first_countable_topology to the HOL image
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move metric_space to its own theory
Fri, 22 Mar 2013 10:41:42 +0100 hoelzl move topological_space to its own theory
Wed, 06 Mar 2013 16:56:21 +0100 hoelzl netlimit is abbreviation for Lim
Wed, 06 Mar 2013 16:56:21 +0100 hoelzl tuned proofs
Wed, 06 Mar 2013 16:56:21 +0100 hoelzl changed continuous_on_intros into a named theorems collection
Wed, 06 Mar 2013 16:56:21 +0100 hoelzl changed continuous_intros into a named theorems collection
Tue, 05 Mar 2013 15:43:22 +0100 hoelzl generalized lemmas in Extended_Real_Limits
Tue, 05 Mar 2013 15:43:21 +0100 hoelzl eventually nhds represented using sequentially
Tue, 05 Mar 2013 15:43:20 +0100 hoelzl generalized compact_Times to topological_space
Tue, 05 Mar 2013 15:43:19 +0100 hoelzl move lemma Inf to usage point
Tue, 05 Mar 2013 15:43:18 +0100 hoelzl tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
Tue, 05 Mar 2013 15:43:17 +0100 hoelzl tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
Tue, 05 Mar 2013 15:43:16 +0100 hoelzl generalized continuous/compact_attains_inf/sup from real to linorder_topology
Tue, 05 Mar 2013 15:43:15 +0100 hoelzl continuity of pair operations
Tue, 05 Mar 2013 15:43:14 +0100 hoelzl use generate_topology for second countable topologies, does not require intersection stable basis
Tue, 05 Mar 2013 15:43:13 +0100 hoelzl generalized isGlb_unique
Wed, 13 Feb 2013 16:35:07 +0100 immler eliminated union_closed_basis; cleanup Fin_Map
Wed, 13 Feb 2013 16:35:07 +0100 immler fine grained instantiations
Wed, 13 Feb 2013 16:35:07 +0100 immler generalized
Wed, 13 Feb 2013 16:35:07 +0100 immler generalized
Thu, 31 Jan 2013 11:31:22 +0100 hoelzl simplify heine_borel type class
Fri, 18 Jan 2013 20:01:59 +0100 hoelzl generalized diameter from real_normed_vector to metric_space
Fri, 18 Jan 2013 20:01:41 +0100 hoelzl tuned proof
Fri, 18 Jan 2013 20:00:59 +0100 hoelzl tune prove compact_eq_totally_bounded
Thu, 17 Jan 2013 15:28:53 -0800 huffman generalized theorem edelstein_fix to class metric_space
Thu, 17 Jan 2013 08:31:16 -0800 huffman simplify proof of compact_imp_bounded
Tue, 15 Jan 2013 20:26:38 -0800 huffman generalize more topology lemmas
Tue, 15 Jan 2013 19:28:48 -0800 huffman generalize topology lemmas; simplify proofs
Thu, 17 Jan 2013 14:38:12 +0100 hoelzl simplified prove of compact_imp_bounded
Thu, 17 Jan 2013 13:58:02 +0100 hoelzl use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
Thu, 17 Jan 2013 13:21:34 +0100 hoelzl move auxiliary lemma to top
Thu, 17 Jan 2013 13:20:17 +0100 hoelzl add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite
Thu, 17 Jan 2013 12:26:54 +0100 hoelzl group compactness-eq-seq-compactness lemmas together
Thu, 17 Jan 2013 12:21:24 +0100 hoelzl replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
Thu, 17 Jan 2013 12:09:48 +0100 hoelzl tuned
Thu, 17 Jan 2013 12:09:21 +0100 hoelzl removed subseq_bigger (replaced by seq_suble)
Thu, 17 Jan 2013 11:59:12 +0100 hoelzl countablility of finite subsets and rational numbers
Tue, 15 Jan 2013 08:29:56 -0800 huffman generalized more topology theorems
Mon, 14 Jan 2013 19:28:39 -0800 huffman generalize lemma islimpt_finite to class t1_space
Mon, 14 Jan 2013 18:30:36 +0100 hoelzl differentiate (cover) compactness and sequential compactness
Mon, 14 Jan 2013 17:53:37 +0100 hoelzl introduce first_countable_topology typeclass
Mon, 14 Jan 2013 17:30:36 +0100 hoelzl move prod instantiation of second_countable_topology to its definition
Mon, 14 Jan 2013 17:29:04 +0100 hoelzl renamed countable_basis_space to second_countable_topology
Fri, 14 Dec 2012 15:46:01 +0100 hoelzl Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
Mon, 03 Dec 2012 18:19:02 +0100 hoelzl add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
Tue, 27 Nov 2012 13:48:40 +0100 immler based countable topological basis on Countable_Set
Fri, 16 Nov 2012 19:14:23 +0100 hoelzl moved (b)choice_iff(') to Hilbert_Choice
Fri, 16 Nov 2012 18:45:57 +0100 hoelzl move theorems to be more generally useable
Fri, 16 Nov 2012 11:22:22 +0100 immler allow arbitrary enumerations of basis in locale for generation of borel sets
less more (0) -100 -60 tip