Members of a Power Set

Stream: new members

[Brandon Sisler]

Hello, I have been trying to state and prove some theorems in Lean, in order to build up my comfort level in the system.

What I would like to prove is that there is no set X, for which (powerset X \subseteq X).
The issue I have been having is if I let X have type set U, then the powerset of X is of the type set set U. So I cannot use the subset relation.

For anyone who can help me I'll put how I wanted to state the theorem so that we can work out which parts to replace.

variable U : Type*
variable X : set U
theorem powerset_not_subset_set : \neq(\powerset X \subseteq X) :=
begin
end

[Matt Diamond]

hello! if you don't mind, could you wrap the code in #backticks? it helps with formatting and makes it easier to open the code in the web editor

[Matt Diamond]

also, you might want to check out docs#Set (which is a ZFC set)

[Adam Topaz]

One way to state this using type theory is to say that there is no injective map from set X to X. But to properly formulate the assertion you mentioned is actually quite non-trivial in type theory (we do have zfc somewhere in mathlib).

[Brandon Sisler]

Oh yes, sure thing

variable U : Type*
variable X : set U
theorem powerset_not_subset_set : \neq(\powerset X \subseteq X) :=
begin
end

[Matt Diamond]

on a side note, I think you may have meant \ne instead of \neq (edit: \not, rather)

[Brandon Sisler]

Adam Topaz
Ahh, that's pretty nifty, thanks!

[Brandon Sisler]

@Matt Diamond
Yes, I think you are right

[Yaël Dillies]

\not rather?

[Matt Diamond]

oh whoops

[Matt Diamond]

yeah, that

[Patrick Johnson]

In set theory it is straightforward:

import set_theory.zfc.basic

example : ¬∃ (a : Set), a.powerset ⊆ a :=
begin
  rintro ⟨a, h⟩,
  refine Set.mem_irrefl _ (@h a _),
  rw Set.mem_powerset,
  refl,
end

[Matt Diamond]

on a side note, does anyone think we should err on the side of not posting complete proofs unless the person specifically asks for one? I'm just thinking about how it can be educational to work things out for yourself, even if it's a bit difficult... but then again, it can also be educational to see how someone else proves it, especially if they're more knowledgeable

(not trying to single Patrick out! his answer just got me thinking about the issue)

[Patrick Johnson]

I'm sorry for posting the proof without a spoiler. I assumed Brandon wants the proof in type theory, so I posted a set-theoretic analogy.