equal
deleted
inserted
replaced
110 by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset) |
110 by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset) |
111 qed |
111 qed |
112 qed |
112 qed |
113 |
113 |
114 |
114 |
115 subsection\<open>Urysohn's lemma (for real^N, where the proof is easy using distances)\<close> |
115 subsection\<open>Urysohn's lemma (for Euclidean spaces, where the proof is easy using distances)\<close> |
116 |
116 |
117 lemma Urysohn_both_ne: |
117 lemma Urysohn_both_ne: |
118 assumes US: "closedin (subtopology euclidean U) S" |
118 assumes US: "closedin (subtopology euclidean U) S" |
119 and UT: "closedin (subtopology euclidean U) T" |
119 and UT: "closedin (subtopology euclidean U) T" |
120 and "S \<inter> T = {}" "S \<noteq> {}" "T \<noteq> {}" "a \<noteq> b" |
120 and "S \<inter> T = {}" "S \<noteq> {}" "T \<noteq> {}" "a \<noteq> b" |