リーンでセットを使用

Question

私は、リーンを使用してトポロジーでいくつかの作業をしたいと思います。

良いスタートとして、私はsets in leanについていくつかの簡単な補題を証明したいと思っていました。

だけ 私は set.unionまたは set.interのためにどこにでも解消ルールを見つけることができない例

def inter_to_union (H : a ∈ set.inter A B) : a ∈ set.union A B := 
    sorry 

または

def set_deMorgan : a ∈ set.inter A B → a ∈ set.compl (set.union (set.compl A) (set.compl B)) := 
sorry 

または、おそらくより興味深いこと

def set_deMorgan2 : set.inter A B = set.compl (set.union (set.compl A) (set.compl B)) := 
sorry 

しかしに関して

ので、私どのようにそれらと仕事をするか分からない。

1. どのように補題を証明できますか？

また、definition of sets in leanを見て、私は非常に多くの紙の数学のように見える構文のビットを、見ることができますが、私は、たとえば、依存型理論のレベルで理解していない：

protected def sep (p : α → Prop) (s : set α) : set α := 
{a | a ∈ s ∧ p a} 

2. どのようにして、上記の例を従属/誘導型のより単純な概念に分解できますか？あなたには、いくつかのx : αあなたは、これをs aを証明することができるためのセットs : set αとを持っている場合は

   def set (α : Type u) := α → Prop 
   

   ：モジュールは、いくつかのタイプα（αは通常、「宇宙」と呼ばれる）に述語とのセットを識別し

Answer 1

'xがsに属している'と解釈されます。この場合

、x ∈ Aは以下のように定義されてset.mem x Aの表記法（私たちは今の型クラスについては気にしないようにしましょう）である：空のセットは常に述語として表現されている理由

protected def mem (a : α) (s : set α) := 
s a 

上記は説明しますfalseを返す：

instance : has_emptyc (set α) := 
⟨λ a, false⟩ 

そしてまた、宇宙は当然そうのように表される：

を

私はどのように最初の補題を証明紹介：

def inter_to_union {α : Type} {A B : set α} {a : α} : A ∩ B ⊆ A ∪ B := 
    assume (x : α) (xinAB : x ∈ A ∩ B),  -- unfold the definition of `subset` 
    have xinA : x ∈ A, from and.left xinAB, 
    @or.inl _ (x ∈ B) xinA 

これは、すべての基本的な集合論におけるこれらの特性のための通常の「好い加減な」証明のようなものです。ここで

set_option pp.notation false 
#print set.sep 

が出力されます：

protected def set.sep : Π {α : Type u}, (α → Prop) → set α → set α := 
λ {α : Type u} (p : α → Prop) (s : set α), 
    set_of (λ (a : α), and (has_mem.mem a s) (p a))