# HG changeset patch # User wenzelm # Date 1468574796 -7200 # Node ID b0f8845e349895e843530ce915e93a7c0911fefb # Parent ac0a3b9c6dae9a8c60a7e99034789c511d326500 proper latex; diff -r ac0a3b9c6dae -r b0f8845e3498 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Fri Jul 15 11:07:51 2016 +0200 +++ b/src/HOL/Topological_Spaces.thy Fri Jul 15 11:26:36 2016 +0200 @@ -1942,7 +1942,8 @@ by (simp add: continuous_within filterlim_at_split) text \ - The following open/closed Collect lemmas are ported from Sébastien Gouëzel's Ergodic_Theory. + The following open/closed Collect lemmas are ported from + Sébastien Gouëzel's \Ergodic_Theory\. \ lemma open_Collect_neq: fixes f g :: "'a::topological_space \ 'b::t2_space"