收敛性和矢量理论
Convergence and vectors theories
Isabelle/HOL有收敛理论吗？我需要定义 ∥x(t)∥ ⟶ 0 as t ⟶ ∞。
另外，我正在寻找向量理论，我找到了一个矩阵理论，但找不到向量理论，Isabelle/HOL中是否存在这样的理论？
干杯。
收敛等在伊莎贝尔中用过滤器表示。 （见对应documentation）
在你的情况下，应该是这样的
filterlim (λt. norm (x t)) (nhds 0) at_top
或者，使用 tendsto 缩写，
((λt. norm (x t)) ⤏ 0) at_top
其中⤏是伊莎贝尔符号\<longlongrightarrow>，可以使用缩写--->.
输入
作为旁注，我想知道你为什么一开始就这样写，因为它等同于
filterlim x (nhds 0) at_top
或者，使用 tendsto 语法：
(x ⤏ 0) at_top
一开始使用这些过滤器进行推理可能会很棘手，但它的优点是为极限和其他拓扑概念提供了统一的框架，一旦掌握了它，就会非常优雅。
至于向量，只需导入 ~~/src/HOL/Analysis/Analysis。那应该有你需要的一切。理想情况下，通过从 isabelle jedit -l HOL-Analysis 开始 Isabelle/jEdit 来构建 HOL-Analysis 会话图像。这样你就不用每次启动系统都要处理所有的Isabelle的分析库了。
我假设“向量”是指具体的有限维实向量 spaces，如 ℝn。这是由 ~~/src/HOL/Analysis/Finite_Cartesian_Product.thy 提供的，它是 HOL-Analysis 的一部分。这提供了 vec 类型，它有两个参数：组件类型（在您的情况下可能是 real）和索引类型，它指定向量的维度 space。
对于每个正整数 n，还有一个预定义类型 n，因此您可以编写例如(real, 3) vec 向量 space ℝ³。还有类型语法，因此您可以为 ('a, 'n) vec.
编写 'a ^ 'n
Isabelle/HOL有收敛理论吗？我需要定义 ∥x(t)∥ ⟶ 0 as t ⟶ ∞。
另外，我正在寻找向量理论，我找到了一个矩阵理论，但找不到向量理论，Isabelle/HOL中是否存在这样的理论？
干杯。
收敛等在伊莎贝尔中用过滤器表示。 （见对应documentation）
在你的情况下，应该是这样的
filterlim (λt. norm (x t)) (nhds 0) at_top
或者，使用 tendsto 缩写，
((λt. norm (x t)) ⤏ 0) at_top
其中⤏是伊莎贝尔符号\<longlongrightarrow>，可以使用缩写--->.
作为旁注，我想知道你为什么一开始就这样写，因为它等同于
filterlim x (nhds 0) at_top
或者，使用 tendsto 语法：
(x ⤏ 0) at_top
一开始使用这些过滤器进行推理可能会很棘手，但它的优点是为极限和其他拓扑概念提供了统一的框架，一旦掌握了它，就会非常优雅。
至于向量，只需导入 ~~/src/HOL/Analysis/Analysis。那应该有你需要的一切。理想情况下，通过从 isabelle jedit -l HOL-Analysis 开始 Isabelle/jEdit 来构建 HOL-Analysis 会话图像。这样你就不用每次启动系统都要处理所有的Isabelle的分析库了。
我假设“向量”是指具体的有限维实向量 spaces，如 ℝn。这是由 ~~/src/HOL/Analysis/Finite_Cartesian_Product.thy 提供的，它是 HOL-Analysis 的一部分。这提供了 vec 类型，它有两个参数：组件类型（在您的情况下可能是 real）和索引类型，它指定向量的维度 space。
对于每个正整数 n，还有一个预定义类型 n，因此您可以编写例如(real, 3) vec 向量 space ℝ³。还有类型语法，因此您可以为 ('a, 'n) vec.
'a ^ 'n