从设置包含到设置精简的平等

给定集合包含的证明及其相反，我希望能够证明两个集合是平等的。从设置包含到设置精简的平等

例如，我知道如何证明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！这是一个更广泛的问题，但功能/命题扩展性的哲学含义是什么？ –

从设置包含到设置精简的平等

回答

相关问题