equal
deleted
inserted
replaced
3289 lemma eventually_filter_from_subbaseI: "P \<in> B \<Longrightarrow> eventually P (filter_from_subbase B)" |
3289 lemma eventually_filter_from_subbaseI: "P \<in> B \<Longrightarrow> eventually P (filter_from_subbase B)" |
3290 by (subst eventually_filter_from_subbase) (auto intro!: exI[of _ "{P}"]) |
3290 by (subst eventually_filter_from_subbase) (auto intro!: exI[of _ "{P}"]) |
3291 |
3291 |
3292 lemma filter_from_subbase_not_bot: |
3292 lemma filter_from_subbase_not_bot: |
3293 "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot" |
3293 "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot" |
3294 unfolding trivial_limit_def eventually_filter_from_subbase by auto |
3294 unfolding trivial_limit_def eventually_filter_from_subbase |
|
3295 bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp |
3295 |
3296 |
3296 lemma closure_iff_nhds_not_empty: |
3297 lemma closure_iff_nhds_not_empty: |
3297 "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})" |
3298 "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})" |
3298 proof safe |
3299 proof safe |
3299 assume x: "x \<in> closure X" |
3300 assume x: "x \<in> closure X" |