说明一个集合分割另一个集合的标准方法是什么

Question

我在数学上写{1, 2} + {3} + {4} = {1, 2, 3, 4}表示LHS上的集合分割RHS上的集合。isabelle也有类似的情况吗?这样我就不需要把所有的排列都看一遍了，{1, 2} intersect {3} = {}等等。

[编辑]

我在概率西格玛代数包中发现了这个disjoint定义，但是有没有什么东西不会引入这种依赖关系?

Answer 1

disjoint可能是最好的选择。你可以把这个定义和后面的几个引理复制到你自己的理论中。

我将与Johannes Hölzl(他制作了概率论库)交谈，并询问他对将disjoint移动到HOL中的想法，以便在没有额外导入的情况下可用

Answer 2

在Isabelle (http://isabelle.in.tum.de/repos/isabelle/rev/53697011b03a)的开发版本中，它现在在自己的理论文件中:

~~/src/HOL/Library/Disjoint_Sets