equal
deleted
inserted
replaced
46 proof - |
46 proof - |
47 have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto |
47 have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto |
48 moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms) |
48 moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms) |
49 ultimately show "open S" by simp |
49 ultimately show "open S" by simp |
50 qed |
50 qed |
|
51 |
|
52 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" |
|
53 by (auto intro: openI) |
51 |
54 |
52 lemma closed_empty [continuous_intros, intro, simp]: "closed {}" |
55 lemma closed_empty [continuous_intros, intro, simp]: "closed {}" |
53 unfolding closed_def by simp |
56 unfolding closed_def by simp |
54 |
57 |
55 lemma closed_Un [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)" |
58 lemma closed_Un [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)" |