changeset 67459 | 7264dfad077c |
parent 67455 | fe6bcf0137b4 |
child 67577 | 0ac53b666228 |
--- a/src/HOL/Analysis/Connected.thy Fri Jan 19 15:42:53 2018 +0100 +++ b/src/HOL/Analysis/Connected.thy Fri Jan 19 15:50:17 2018 +0100 @@ -1292,7 +1292,7 @@ definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)" -lemma bdd_below_infdist[intro, simp]: "bdd_below (dist x`A)" +lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)" by (auto intro!: zero_le_dist) lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a:A. dist x a)"