论文标题
Mathlib中积分变量公式的更改的形式化
A formalization of the change of variables formula for integrals in mathlib
论文作者
论文摘要
我们报告了Mathlib库中的变量公式变化的形式化。我们对该定理的版本非常笼统，并基于线性代数，分析，衡量理论和描述性集理论的发展。由于Mathlib的高度集成开发模型，这些域之间的相互作用是透明的。
We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on developments in linear algebra, analysis, measure theory and descriptive set theory. The interplay between these domains is transparent thanks to the highly integrated development model of mathlib.
