我有一个定义为f的关系f: A -> B×C。我想写一个一阶公式,将这个关系限制为从A到B×C的双射函数。∀a: A,∃!bc :B×C,f(a)=bc -- f is function∀(b,c):b×C,∃a: A,f(a)=bc -- f is surjective
正如你所看到的,上面的公式是高阶逻
我刚从伊莎贝尔开始我的第一步,但是,对于定理证明器和证明助手来说,我有点迷失了。我主要对函数式分析或代数的应用程序感兴趣--我看过这些文档,我试图用语言环境来获得我自己的例子,但我遇到了一些非常基本的问题。lemma assoc_general: "b x (a x c) = (b x a) x c" done
这只是一个证明,但我不能让伊莎贝尔工作证明命令在“
我想证明nat的高斯定理。Require Import NPeano.Theorem Gauss_nat: forall (a b c:nat), gcd a b = 1 -> (a | (b*c)) -> (a | c).
该定理已经针对整数Z进行了定义,请参阅。到目前为止,我得到的建议是使用Bezout引理,该引理指出