セット組み込みからリーンの等価設定へ

Question

セット組み込みとその逆の証明が与えられていると、2つのセットが等しいことを示すことができます。

は例えば、私は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 

は、これら2つの封入証明を考えると、私は設定平等を証明しない方法、すなわち

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

Answer 1

あなたがしたいと思うでしょう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の証明からわかるように、機能的および命題的な内在性の両方を兼ね備えています。