A Missing Lemma Dual to Lim_right_bound
伊藤洋介
glacier345 at gmail.com
Tue May 6 08:30:56 CEST 2025
Dear Isabelle developers,
There is the lemma Lim_right_bound in HOL/Analysis/Elementary_Topology.thy:
```
lemma Lim_right_bound:
fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder,
no_top} \<Rightarrow>
'b::{linorder_topology, conditionally_complete_linorder}"
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"
and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow>
K \<le> f a"
shows "(f \<longlongrightarrow> Inf (f ` ({x<..} \<inter> I))) (at x
within ({x<..} \<inter> I))"
```
However, the dual of this lemma (on the left-hand limit) is missing.
Could you consider adding the following code to Elementary_Topology.thy?
If there is an appropriate way to suggest improvements, please let me know.
```
lemma Lim_left_bound:
fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder,
no_bot} \<Rightarrow>
'b :: {linorder_topology, conditionally_complete_linorder}"
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"
and bnd: "\<And>b. b \<in> I \<Longrightarrow> b < x \<Longrightarrow>
f b \<le> K"
shows "(f \<longlongrightarrow> Sup (f ` ({..<x} \<inter> I))) (at x
within ({..<x} \<inter> I))"
proof (cases "{..<x} \<inter> I = {}")
case True
then show ?thesis by simp
next
case False
show ?thesis
proof (rule order_tendstoI)
fix b
assume b: "Sup (f ` ({..<x} \<inter> I)) < b"
{
fix y
assume "y \<in> {..<x} \<inter> I"
with False bnd have "f y \<le> Sup (f ` ({..<x} \<inter> I))" by
(auto intro!: cSup_upper bdd_aboveI2)
with b have "f y < b" by order
}
then show "eventually (\<lambda>x. f x < b) (at x within ({..<x}
\<inter> I))"
by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
next
fix b
assume "b < Sup (f ` ({..<x} \<inter> I))"
from less_cSupD[OF _ this] False obtain y where y: "y < x" "y \<in> I"
"b < f y" by auto
then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> b < f x)
(at_left x)"
unfolding eventually_at_right[OF \<open>y < x\<close>]
by (smt (verit, best) assms(1) basic_trans_rules(23)
eventually_at_left less_le not_le)
then show "eventually (\<lambda>x. b < f x) (at x within ({..<x}
\<inter> I))"
unfolding eventually_at_filter by eventually_elim simp
qed
qed
```
Best regards,
--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345 at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250506/16981701/attachment.htm>
More information about the isabelle-dev
mailing list