證明兩個特定集合在Isabelle中具有相同的基數

Question

我很難證明兩個集合具有相同的基數。 以下所有集合都是有限的。

首先假設我們已經設定了（M :: b集合）和函數foo ::「b集合⇒b集合⇒bool」
使得（foo AC = foo BC⟷A = B）和對於M中的每一個A，實際上都有一個C，這樣foo A.C.

我試圖證明那張卡{S。 ∃A∈M。 （S = {C.foo A C}）} = card M. 對此的非正式證明是顯而易見的，但我似乎無法在Isabelle找到有效的證據 ;既不是≤也不是≥部分。

Answer 1

好吧，所以第一步是你應該用更方便的方式寫下這個集合理解{S. ∃A∈M. (S = {C. foo A C}) }。第一步將是{{C. foo A C} |A. A ∈ M}，但我會建議使用「設置圖像」運營商：

lemma "{S. ∃A∈M. (S = {C. foo A C})} = (λA. {C. foo A C}) ` M" by blast 

然後，你可以簡單地使用的事實，(λA. {C. foo A C})是單射和規則card_image，它說，圖像的基數內集函數的集合與原集合的集合相同：

lemma 
    assumes "⋀A B C. A ∈ M ⟹ B ∈ M ⟹ foo A C = foo B C ⟷ A = B" 
    shows "card {S. ∃A∈M. (S = {C. foo A C})} = card M" 
proof - 
    have "{S. ∃A∈M. (S = {C. foo A C})} = (λA. {C. foo A C}) ` M" 
    by blast 
    also have "inj_on (λA. {C. foo A C}) M" 
    using assms by (auto simp: inj_on_def) 
    hence "card ((λA. {C. foo A C}) ` M) = card M" 
    by (rule card_image) 
    finally show ?thesis . 
qed