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