我如何在Isabelle中证明简单的lemma cd : "card {m∈ℕ. m <4} = 4"语句?auto对我没有帮助,奇怪的是sledgehammer超时了(即使我在右边使用了不同的值,比如3或5,以确保我没有忽略一些技术上的Isabelle细节,这些细节实际上可能会使基数计算为这些数字之一)。我的印象是,我必须使用一些引理(或从Set_Interval.thy中获得灵感),因为这些类型的集合被广泛使用,但到目前为
引理without_P的意思是:如果你知道(有限的)集mnnat不是空的,那么在将f映射到mnnat之后,mnnat中必须存在一个元素,即最小的元素。我们知道mnnat是有限的,因为其中有n-1数,在without_P证明的上下文中,我们也知道mnnat不是空的,因为前提是(exists x : mnnat, True)。现在,mnnat是非空和