От включения набора для установления равенства в Lean

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, он сочетает в себе функциональную и пропозициональную экстенсиональность.