Isabelle 中的连续函数

Question

我想在实线的区间上定义一个连续函数 - [a,b)、[a,b]、(a,b) 或 (a,b]（其中 a < b and either could possibly be infinite) -- in Isabelle, or state that a function is continuous on such an interval.

我相信我想要的是 Continuous_on s f 因为

“连续_on s f ⟷ (∀x∈s。(f ⤏ f x)（在 s 内的 x 处）”

（我从这里得到的：https://isabelle.in.tum.de/library/HOL/HOL/Topological_Spaces.html#Topological_Spaces.topological_space_class.at_within|const）

所以我认为“s”应该是一个间隔，但我不确定如何最好地表示它。

所以我想知道如何将“s”设置为上面列出的任何类型的设置间隔。 谢谢！

Answer 1

你的问题的答案

在每个有序类型中，您可以为从

{a..b}

到

a

的闭区间编写

b

。对于开放/半开放变体，有

{a<..b}

、

{a..<b}

、

{a<..<b}

、

{a..}

、

{..b}

、

{a<..}

和

{..<b}

。

这些在

HOL.Set_Interval

中定义，它们的内部名称是

lessThan

、

atLeastAtMost

等。

因此，就您而言，您可以简单地写下类似

continuous_on {a..b} f

的内容。

理解如何在定理证明中有效地进行关于极限、连续性等的论证需要一些时间。不要害怕在这里或在 Zulip 上提问。当然，你总是可以用困难的方式做事（例如 ε-δ 推理），但是一旦你更加熟练地使用库，很多事情就会变得容易得多。这让我想到：

附录：过滤器

但请注意，要真正以惯用的方式推理伊莎贝尔的连续性，您必须理解过滤器，这是（除其他外）讨论“点的邻域”的一种方式。有一个定义

continuous

，它在过滤器处接受一个函数，可以用来表示函数在某些条件下在给定点上是连续的。

比如有滤镜

• nhds x

  ，描述了

  x

  的邻域（即距离

  x

  足够近的所有内容）

• at x within A

  ，它描述了

  x

  与

  A

  相交的尖邻域 - 即，您接近

  x

  而没有完全到达它，同时完全保持在集合

  A

内

• at x

  ，简单来说就是

  at x within UNIV

  ，即

  x

  的尖邻域，没有进一步的限制

• at_left x

  和

  at_right x

  例如实数，定义为

  at x within {..<x}

  和

  at x within {x<..}

  ，即

  x

的左右邻域

然后您可以写类似

continuous (at x) F

或

continuous (at_right x) F

之类的内容。如果我没记错的话，

continuous_on A f

相当于

∀x∈A. continuous (at x within A) f

。

过滤器对于许多其他相关事物也很有用，例如极限、开/闭集、一致连续性和导数。

本文解释了如何在 Isabelle 分析库中使用过滤器。它还有一个关于连续性的简短部分。