從設置包含到設置精簡的平等

給定集合包含的證明及其相反，我希望能夠證明兩個集合是平等的。從設置包含到設置精簡的平等

例如，我知道如何證明following statement，並its converse：

open set 

universe u 
variable elem_type : Type u 
variable A : set elem_type 
variable B : set elem_type 

def set_deMorgan_incl : A ∩ B ⊆ set.compl ((set.compl A) ∪ (set.compl B)) := 
    sorry

鑑於這兩個包容證明，我怎麼證明設置的平等，即

def set_deMorgan_eq : A ∩ B = set.compl ((set.compl A) ∪ (set.compl B)) := 
    sorry

來源

2017-08-13 Adam Kurkiewicz

你會想使用子集關係的反對稱性，如已證明in the stdlib package：

def set_deMorgan_eq : A ∩ B = set.compl ((set.compl A) ∪ (set.compl B)) := 
subset.antisymm (set_deMorgan_incl _ _ _) (set_deMorgan_incl_conv _ _ _)

正如你可以在subset.antisymm的證明中看到的那樣，它結合了功能性和命題性的擴展性。

來源

2017-08-13 11:24:29

謝謝，我沒有意識到這需要stdlib！這是一個更廣泛的問題，但功能/命題擴展性的哲學含義是什麼？ –

從設置包含到設置精簡的平等

回答

相關問題