summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Topological_Spaces.thy

changeset 52729 | 412c9e0381a1 |

parent 52265 | bb907eba5902 |

child 53215 | 5e47c31c6f7c |

1.1 --- a/src/HOL/Topological_Spaces.thy Wed Jul 24 17:15:59 2013 +0200 1.2 +++ b/src/HOL/Topological_Spaces.thy Thu Jul 25 08:57:16 2013 +0200 1.3 @@ -471,27 +471,28 @@ 1.4 unfolding le_filter_def by simp } 1.5 { assume "F \<le> F'" and "F' \<le> F" thus "F = F'" 1.6 unfolding le_filter_def filter_eq_iff by fast } 1.7 - { show "F \<le> top" 1.8 - unfolding le_filter_def eventually_top by (simp add: always_eventually) } 1.9 - { show "bot \<le> F" 1.10 - unfolding le_filter_def by simp } 1.11 - { show "F \<le> sup F F'" and "F' \<le> sup F F'" 1.12 - unfolding le_filter_def eventually_sup by simp_all } 1.13 - { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''" 1.14 - unfolding le_filter_def eventually_sup by simp } 1.15 { show "inf F F' \<le> F" and "inf F F' \<le> F'" 1.16 unfolding le_filter_def eventually_inf by (auto intro: eventually_True) } 1.17 { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''" 1.18 unfolding le_filter_def eventually_inf 1.19 by (auto elim!: eventually_mono intro: eventually_conj) } 1.20 + { show "F \<le> sup F F'" and "F' \<le> sup F F'" 1.21 + unfolding le_filter_def eventually_sup by simp_all } 1.22 + { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''" 1.23 + unfolding le_filter_def eventually_sup by simp } 1.24 + { assume "F'' \<in> S" thus "Inf S \<le> F''" 1.25 + unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 1.26 + { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S" 1.27 + unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 1.28 { assume "F \<in> S" thus "F \<le> Sup S" 1.29 unfolding le_filter_def eventually_Sup by simp } 1.30 { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'" 1.31 unfolding le_filter_def eventually_Sup by simp } 1.32 - { assume "F'' \<in> S" thus "Inf S \<le> F''" 1.33 - unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 1.34 - { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S" 1.35 - unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } 1.36 + { show "Inf {} = (top::'a filter)" 1.37 + by (auto simp: top_filter_def Inf_filter_def Sup_filter_def) 1.38 + (metis (full_types) Topological_Spaces.top_filter_def always_eventually eventually_top) } 1.39 + { show "Sup {} = (bot::'a filter)" 1.40 + by (auto simp: bot_filter_def Sup_filter_def) } 1.41 qed 1.42 1.43 end