dependent-type - 从集合包含到在精益中设置平等

Question

给定集合包含的证明及其反面，我希望能够证明两个集合是相等的。

例如，我知道如何证明以下陈述及其相反的陈述：

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

Answer 1

您将需要使用子集关系的反对称，如包中所证明的stdlib：

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，它结合了函数和命题的外延性。