Lean4中证明s≠(sᶜ)的相关问题：无需xInU假设可行吗？

问题1：能否不添加xInU假设证明任意集合s满足s ≠ sᶜ？ #

不能直接完成这个证明。原因在于：如果类型α是空类型（不存在任何元素），那么Set.univ是空集，此时所有集合s都只能是空集，它的补集sᶜ同样是空集，这时候s = sᶜ是成立的。

只有当类型α非空时，才能证明s ≠ sᶜ——此时可以取α中的某个元素x，根据排中律，x ∈ s和x ∉ s必有一个成立，由此就能推出s和它的补集不可能相等。如果不添加xInU假设（本质上就是不假定α非空），原命题在空类型场景下不成立，自然无法完成证明。

问题2：任意类型的Set.univ是否至少包含一个元素？是否需要为α类型添加非空约束？ #

不是所有类型的Set.univ都有元素：

• 当α是空类型时，Set.univ就是空集，没有任何元素；
• 只有当α是非空类型（即存在x : α）时，Set.univ才至少包含一个元素。

因此，如果需要Set.univ非空，必须为α添加Nonempty α的约束。

内容的提问来源于stack exchange，提问作者DBE