equal
deleted
inserted
replaced
21 by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) |
21 by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def) |
22 |
22 |
23 lemma compact_eq_closed: |
23 lemma compact_eq_closed: |
24 fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
24 fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
25 shows "compact S \<longleftrightarrow> closed S" |
25 shows "compact S \<longleftrightarrow> closed S" |
26 using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed |
26 using closed_Int_compact[of S, OF _ compact_UNIV] compact_imp_closed |
27 by auto |
27 by auto |
28 |
28 |
29 lemma closed_contains_Sup_cl: |
29 lemma closed_contains_Sup_cl: |
30 fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
30 fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set" |
31 assumes "closed S" |
31 assumes "closed S" |