2110 then obtain b where "b < Inf A" "{b <.. Inf A} \<subseteq> A" |
2110 then obtain b where "b < Inf A" "{b <.. Inf A} \<subseteq> A" |
2111 using open_left[of A "Inf A" x] assms by auto |
2111 using open_left[of A "Inf A" x] assms by auto |
2112 with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A" |
2112 with dense[of b "Inf A"] obtain c where "c < Inf A" "c \<in> A" |
2113 by (auto simp: subset_eq) |
2113 by (auto simp: subset_eq) |
2114 then show False |
2114 then show False |
2115 using cInf_lower[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le) |
2115 using cInf_lower[OF `c \<in> A`] bnd by (metis not_le less_imp_le bdd_belowI) |
2116 qed |
2116 qed |
2117 |
2117 |
2118 lemma Sup_notin_open: |
2118 lemma Sup_notin_open: |
2119 assumes A: "open A" and bnd: "\<forall>a\<in>A. a < x" |
2119 assumes A: "open A" and bnd: "\<forall>a\<in>A. a < x" |
2120 shows "Sup A \<notin> A" |
2120 shows "Sup A \<notin> A" |
2123 then obtain b where "Sup A < b" "{Sup A ..< b} \<subseteq> A" |
2123 then obtain b where "Sup A < b" "{Sup A ..< b} \<subseteq> A" |
2124 using open_right[of A "Sup A" x] assms by auto |
2124 using open_right[of A "Sup A" x] assms by auto |
2125 with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A" |
2125 with dense[of "Sup A" b] obtain c where "Sup A < c" "c \<in> A" |
2126 by (auto simp: subset_eq) |
2126 by (auto simp: subset_eq) |
2127 then show False |
2127 then show False |
2128 using cSup_upper[OF `c \<in> A`, of x] bnd by (metis less_imp_le not_le) |
2128 using cSup_upper[OF `c \<in> A`] bnd by (metis less_imp_le not_le bdd_aboveI) |
2129 qed |
2129 qed |
2130 |
2130 |
2131 end |
2131 end |
2132 |
2132 |
2133 instance linear_continuum_topology \<subseteq> perfect_space |
2133 instance linear_continuum_topology \<subseteq> perfect_space |
2149 fix x y assume "x < y" "x \<in> A" "y \<in> B" "x \<in> U" "y \<in> U" |
2149 fix x y assume "x < y" "x \<in> A" "y \<in> B" "x \<in> U" "y \<in> U" |
2150 |
2150 |
2151 let ?z = "Inf (B \<inter> {x <..})" |
2151 let ?z = "Inf (B \<inter> {x <..})" |
2152 |
2152 |
2153 have "x \<le> ?z" "?z \<le> y" |
2153 have "x \<le> ?z" "?z \<le> y" |
2154 using `y \<in> B` `x < y` by (auto intro: cInf_lower[where z=x] cInf_greatest) |
2154 using `y \<in> B` `x < y` by (auto intro: cInf_lower cInf_greatest) |
2155 with `x \<in> U` `y \<in> U` have "?z \<in> U" |
2155 with `x \<in> U` `y \<in> U` have "?z \<in> U" |
2156 by (rule *) |
2156 by (rule *) |
2157 moreover have "?z \<notin> B \<inter> {x <..}" |
2157 moreover have "?z \<notin> B \<inter> {x <..}" |
2158 using `open B` by (intro Inf_notin_open) auto |
2158 using `open B` by (intro Inf_notin_open) auto |
2159 ultimately have "?z \<in> A" |
2159 ultimately have "?z \<in> A" |
2161 |
2161 |
2162 { assume "?z < y" |
2162 { assume "?z < y" |
2163 obtain a where "?z < a" "{?z ..< a} \<subseteq> A" |
2163 obtain a where "?z < a" "{?z ..< a} \<subseteq> A" |
2164 using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto |
2164 using open_right[OF `open A` `?z \<in> A` `?z < y`] by auto |
2165 moreover obtain b where "b \<in> B" "x < b" "b < min a y" |
2165 moreover obtain b where "b \<in> B" "x < b" "b < min a y" |
2166 using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B` |
2166 using cInf_less_iff[of "B \<inter> {x <..}" "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B` |
2167 by (auto intro: less_imp_le) |
2167 by (auto intro: less_imp_le) |
2168 moreover have "?z \<le> b" |
2168 moreover have "?z \<le> b" |
2169 using `b \<in> B` `x < b` |
2169 using `b \<in> B` `x < b` |
2170 by (intro cInf_lower[where z=x]) auto |
2170 by (intro cInf_lower) auto |
2171 moreover have "b \<in> U" |
2171 moreover have "b \<in> U" |
2172 using `x \<le> ?z` `?z \<le> b` `b < min a y` |
2172 using `x \<le> ?z` `?z \<le> b` `b < min a y` |
2173 by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le) |
2173 by (intro *[OF `x \<in> U` `y \<in> U`]) (auto simp: less_imp_le) |
2174 ultimately have "\<exists>b\<in>B. b \<in> A \<and> b \<in> U" |
2174 ultimately have "\<exists>b\<in>B. b \<in> A \<and> b \<in> U" |
2175 by (intro bexI[of _ b]) auto } |
2175 by (intro bexI[of _ b]) auto } |