在精益中使用集合

我想用精益做一些拓撲工作。在精益中使用集合

作爲一個好的開始，我想證明一些關於sets in lean的簡單引理。

例如

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

但我不能只找到set.union或set.inter隨時隨地刪除規則，所以我不知道如何與他們合作。

如何證明引理句？

而且，看着definition of sets in lean，我可以看到語法的位，這看起來非常像紙數學，但我完全不依賴型理論層面理解，例如：

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

如何將上述例子分解爲依賴/歸納類型的簡單概念？

來源

2017-08-11 Adam Kurkiewicz

我問[一個單獨的問題] （https://stackoverflow.com/questions/45658919/from-set-inclusion-to-set-equality-in-lean）關於最後一個引理 –

該模塊識別與某種類型的α謂詞集（α通常被稱爲「宇宙」）：

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

如果您有一組s : set α和一些x : α可以證明s a，這被解釋爲'x屬於s'。

在這種情況下，x ∈ A是一個符號（讓我們不要介意類型類現在）爲set.mem x A其定義如下：

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

以上解釋了爲什麼空集始終表示爲謂語返回false：

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

而且也，宇宙是意料之中表示，像這樣：

def univ : set α := 
λ a, true

我將展示如何證明第一個引理：

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

這一切都像在基本集合論這些屬性通常的「貼題」的證明。

關於你的問題有關sep - 您可以通過符號看到像這樣：

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))

來源

2017-08-11 12:06:20

謝謝，迄今爲止這非常有幫助。你怎麼知道x∈A是'mem x A'的符號？你找到一個文件，引入了這個符號嗎？ –

你的'inter_to_union'證明的最後一行可以簡化爲：'or.intro_left（x∈B）xinA' –

哦，我可以看到'x∈A'問題的答案：只需鍵入'set_option pp.notation false #print∈' –

在精益中使用集合

回答

相關問題