1

我想用精益做一些拓扑工作。

作为一个好的开始，我想证明几个关于精益集合的简单引理。

例如

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.unionor的消除规则set.inter，所以我只是不知道如何使用它们。

  1. 我如何证明引理？

另外，查看lean 中集合的定义，我可以看到一些语法，看起来很像纸上数学，但我在依赖类型理论的层面上不理解，例如：

protected def sep (p : α → Prop) (s : set α) : set α :=
{a | a ∈ s ∧ p a}
  1. 如何将上述示例分解为更简单的依赖/归纳类型概念？
4

1 回答 1

2

该模块使用某种类型的谓词识别集合α（α通常称为“宇宙”）：

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-11T12:06:20.950 回答