从集合包含到精益平等

作者: v-star*위위
发布时间: 2024-04-20 12:25:13 (3天前)
转自：

2 条回复

0#
回复此人
不易青年。 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 正如所证明的那样，您将希望使用子集关系的反对称性 <a href="https://github.com/leanprover/stdlib/blob/6d9072821b60d6a4a7293c943c07fba65041f25e/data/set/basic.lean#L44" rel="nofollow noreferrer"> 在里面 <code> stdlib </code> 包 </A> ： </p> <pre> <code> def set_deMorgan_eq : A �� B = set.compl ((set.compl A) �� (set.compl B)) := subset.antisymm (set_deMorgan_incl _ _ _) (set_deMorgan_incl_conv _ _ _) </code> </pre> <P> 正如你在证明中看到的那样 <code> subset.antisymm </code> ，它结合了功能和命题的扩展性。 </p> </DIV>

编辑

登录后才能参与评论