<div dir="ltr"><div>Dear Isabelle developers,</div><div><br></div><div>There is the lemma Lim_right_bound in HOL/Analysis/Elementary_Topology.thy:</div><div>```</div><div>lemma Lim_right_bound:<br>  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow><br>    'b::{linorder_topology, conditionally_complete_linorder}"<br>  assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"<br>    and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"<br>  shows "(f \<longlongrightarrow> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"</div><div>```</div><div>However, the dual of this lemma (on the left-hand limit) is missing.</div><div>Could you consider adding the following code to Elementary_Topology.thy?</div><div>If there is an appropriate way to suggest improvements, please let me know.</div><div>```</div><div>lemma Lim_left_bound:<br>  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_bot} \<Rightarrow><br>    'b :: {linorder_topology, conditionally_complete_linorder}"<br>  assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> b < x \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"<br>    and bnd: "\<And>b. b \<in> I \<Longrightarrow> b < x \<Longrightarrow> f b \<le> K"<br>  shows "(f \<longlongrightarrow> Sup (f ` ({..<x} \<inter> I))) (at x within ({..<x} \<inter> I))"<br>proof (cases "{..<x} \<inter> I = {}")<br>  case True<br>  then show ?thesis by simp<br>next<br>  case False<br>  show ?thesis<br>  proof (rule order_tendstoI)<br>    fix b<br>    assume b: "Sup (f ` ({..<x} \<inter> I)) < b"<br>    {<br>      fix y<br>      assume "y \<in> {..<x} \<inter> I"<br>      with False bnd have "f y \<le> Sup (f ` ({..<x} \<inter> I))" by (auto intro!: cSup_upper bdd_aboveI2)<br>      with b have "f y < b" by order<br>    }<br>    then show "eventually (\<lambda>x. f x < b) (at x within ({..<x} \<inter> I))"<br>      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)<br>  next<br>    fix b<br>    assume "b < Sup (f ` ({..<x} \<inter> I))"<br>    from less_cSupD[OF _ this] False obtain y where y: "y < x" "y \<in> I" "b < f y" by auto<br>    then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> b < f x) (at_left x)"<br>      unfolding eventually_at_right[OF \<open>y < x\<close>]<br>      by (smt (verit, best) assms(1) basic_trans_rules(23) eventually_at_left less_le not_le)<br>    then show "eventually (\<lambda>x. b < f x) (at x within ({..<x} \<inter> I))"<br>      unfolding eventually_at_filter by eventually_elim simp<br>  qed<br>qed<br>```</div><div><br></div><div>Best regards,<div></div><br><span class="gmail_signature_prefix">-- </span><br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div>伊藤 洋介</div><div>Yosuke ITO<br></div><div>+81 80-5057-6931</div><div><a href="mailto:glacier345@gmail.com" target="_blank">glacier345@gmail.com</a></div><div><br></div></div></div></div></div><div><br></div></div>