equal
deleted
inserted
replaced
8 section \<open>Limits on the Extended real number line\<close> |
8 section \<open>Limits on the Extended real number line\<close> |
9 |
9 |
10 theory Extended_Real_Limits |
10 theory Extended_Real_Limits |
11 imports |
11 imports |
12 Topology_Euclidean_Space |
12 Topology_Euclidean_Space |
13 "~~/src/HOL/Library/Extended_Real" |
13 "HOL-Library.Extended_Real" |
14 "~~/src/HOL/Library/Extended_Nonnegative_Real" |
14 "HOL-Library.Extended_Nonnegative_Real" |
15 "~~/src/HOL/Library/Indicator_Function" |
15 "HOL-Library.Indicator_Function" |
16 begin |
16 begin |
17 |
17 |
18 lemma compact_UNIV: |
18 lemma compact_UNIV: |
19 "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" |
19 "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" |
20 using compact_complete_linorder |
20 using compact_complete_linorder |