在精益中使用集合

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

作为一个好的开始，我想证明一些关于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∈' –

在精益中使用集合

回答

相关问题