问关于集合内容的命题

EN

你是在类型理论中，所以子集的概念并不完全以集合论的方式存在。

将某事物描述为nat的子集是通过将它描述为对自然数的一个命题来完成的。某种类型的nat -> Prop。

让H是nat的子集的句子是这样写的：

Variable H : nat -> Prop.

现在，关于自然数的谓词只能应用于自然数。

如果您希望具有一致性，并讨论自然数的全部子集，则表示为(随机选择名称)。

Definition all_nat n := True.

将注意力转到您的myProp谓词上，它将只应用于自然数上的谓词，因此您可以删除有关作为nat子集的部分，而nat的子集总是会满足的。

Definition myProp (H : nat -> Prop) := forall x, H (2 * x) -> H x.

如果我真的想按照你最初的建议做一个描述，我会写

Definition myProp' (H : nat -> Prop) :=
   (forall x, H x -> all_nat x) /\
   (forall x, H (2 * x) -> H x).

但是，在all_nat的情况下，连词的第一部分实际上是无用的。在其他情况下，如果您想要考虑另一个有意义的nat子集的所有子集，它可能会派上用场。