如何在Isabelle中用continuous_on定义实轴各类区间上的连续函数？

要在Isabelle中声明或证明函数在实轴各类区间上的连续性，你完全可以使用continuous_on s f，其中关键是用Isabelle标准库提供的集合表示来定义区间参数s。以下是各类区间的标准写法，结合continuous_on的使用示例：

一、有限端点的区间表示 #

假设a和b是实数，且满足a < b，对应区间的写法如下：

• 闭区间 [a, b]
  手写集合表达式：{x. a ≤ x ∧ x ≤ b}
  标准库函数（需导入HOL-Analysis.Interval）：closed_interval a b
  示例：

  lemma continuous_on_closed:
    fixes a b :: real and f :: "real ⇒ real"
    assumes "a < b"
    shows "continuous_on (closed_interval a b) f"
  

• 开区间 (a, b)
  手写集合表达式：{x. a < x ∧ x < b}
  标准库函数：open_interval a b
  示例：

  lemma continuous_on_open:
    fixes a b :: real and f :: "real ⇒ real"
    assumes "a < b"
    shows "continuous_on (open_interval a b) f"
  

• 左闭右开区间 [a, b)
  手写集合表达式：{x. a ≤ x ∧ x < b}
  标准库函数：left_closed_interval a b
  示例：

  lemma continuous_on_left_closed:
    fixes a b :: real and f :: "real ⇒ real"
    assumes "a < b"
    shows "continuous_on (left_closed_interval a b) f"
  

• 左开右闭区间 (a, b]
  手写集合表达式：{x. a < x ∧ x ≤ b}
  标准库函数：right_closed_interval a b
  示例：

  lemma continuous_on_right_closed:
    fixes a b :: real and f :: "real ⇒ real"
    assumes "a < b"
    shows "continuous_on (right_closed_interval a b) f"
  

二、含无穷端点的区间表示 #

Isabelle用at_top表示正无穷方向，at_bot表示负无穷方向，对应区间可以用标准库的集合缩写或手写表达式：

• [a, ∞)：Ici a（标准库缩写，等价于{x. a ≤ x}）
• (-∞, b]：Iic b（等价于{x. x ≤ b}）
• (a, ∞)：Ioi a（等价于{x. a < x}）
• (-∞, b)：Iio b（等价于{x. x < b}）
• 整个实轴 (-∞, ∞)：UNIV :: real set

示例：证明函数在[0, ∞)上连续

lemma continuous_on_nonneg:
  fixes f :: "real ⇒ real"
  shows "continuous_on (Ici 0) f"

三、注意事项 #

1. 库导入：要使用上述标准库区间函数和集合缩写，需在理论文件开头添加导入：

   imports
     HOL-Analysis
   begin
   

2. 端点条件：有限区间需满足a < b，否则区间为空集，continuous_on在空集上默认成立（全称量词空真）。
3. 推理便利性：优先使用标准库提供的区间函数（如closed_interval）或集合缩写（如Ici），这些表达式自带拓扑性质（如闭集、开集），便于后续调用相关定理进行推理。

内容的提问来源于stack exchange，提问作者Squirtle