我想在使用精益的拓扑中做一些工作。
作为一个良好的开端,我想证明一些关于精益集合的简单引理。
例如
def inter_to_union(H:a set.interA B):a set….
该模块使用某种类型的谓词来标识集合 �� ( �� 通常被称为“宇宙”):
��
def set (�� : Type u) := �� �� Prop
如果你有一套 s : set �� 对某些人来说 x : �� 你可以证明 s a ,这被解释为'x属于s'。
s : set ��
x : ��
s a
在这种情况下, x �� A 是一种符号(让我们不要介意现在的类型类) set.mem x A 其定义如下:
x �� A
set.mem x A
protected def mem (a : ��) (s : set ��) := s a
以上解释了为什么空集表示为始终返回的谓词 false :
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 - 你可以看到这样的符号:
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))