Set theory game

Stream: new members

[Daniil Zhitov]

Hi everyone. I am stuck on the final level of the Set Theory Game. It says that for a for a set A, such that for any family of sets F such that \U0 F = A A\in F, A must be a singleton. (A : Set U) (h1 : ∀ F, (⋃₀ F = A → A ∈ F)) : ∃ x, A = {x}. It seems to me that it is not true if A is the empty set. Then it is only possible that F contains the empty set and no other sets. However, the empty set is not a singleton. Am I missing something?
image.png

[Kevin Buzzard]

Yes, F might be the empty set (and hence F would not contain the empty set, because F contains no sets at all).

[Richard Osborn]

I believe he is asking when F = {∅}. The issue is that h1 requires you to provide an F and a proof that ⋃₀ F = A. This proof is impossible to provide when F = {∅}, so you can never satisfy h1 {∅}.

[Daniil Zhitov]

I missed the possibility of F being the empty set rather than F = {∅} indeed. I think F = ∅ could be used at h1 and leads to a contradiction with A \in \emptyset.

[Daniil Zhitov]

I can't really make this work though. I am stuck at trying to prove False from x\in\emptyset.

[Richard Osborn]

What do you have so far? You should be trying to construct an F that you can show its union is equal to A.

[Kevin Buzzard]

I know from the way Lean implements the empty set that x \in \emptyset is definitionally equal to False.

[Daniil Zhitov]

Indeed!

[Richard Osborn]

If you try to use F = ∅, you'll also run into problems proving ⋃₀ F = A.

[Daniil Zhitov]

hmmm

[Daniil Zhitov]

My idea is that for F =\empty the \U0 will produce empty. Thus \U0 F = A so A\in\empty (of the universe of families). Contradictory as desired.

[Daniil Zhitov]

I am trying to implement this right now.

[Richard Osborn]

The issue you are going to run into is the fact that you need to provide the proof of ⋃₀ F = A. It is not a consequence.

[Daniil Zhitov]

In case A is empty, applying F empty would prove this result. Thus, A in empty. I am repeating the same thing so sorry if am missing something.

[Daniil Zhitov]

I've managed to do the case with A empty entirely. Now the only challenge is so get an element y from the non-empty A.

[Daniil Zhitov]

code for this
part if you are interested is

have h2 := h1 {s | ∀ x1∈A, s={x1}}
by_cases hE : A = ∅
have hE1 : False
apply h1 ∅
ext y
rw [mem_sUnion]
apply Iff.intro
intro h
obtain ⟨t,ht⟩ := h
cases' ht with h3 h4
cases' h3
intro h
rw [hE] at h
cases' h
cases' hE1

[Daniil Zhitov]

I have managed to obtain an element from non-empty A. I think I should be able to get it from there. Thank you guys!

[Richard Osborn]

You'll find that proving A ≠ ∅ is unnecessary once you figure out the rest of the proof. Also, using F = ∅ gives a fairly short 1 liner that A ≠ ∅.

example (A : Set U) (h1 : ∀ F, (⋃₀ F = A → A ∈ F)) : A ≠ ∅ :=
  fun h => h1 ∅ (by simp only [Set.sUnion_empty, h])

[Dan Velleman]

In your first step, I don't think you've made the best choice of the set to apply h1 to. The hint suggests that you should appy h1 to a family of sets with two properties, and the first property is that the union of the family must be A. For your choice, that might not be true. It might help to think about this example: Suppose that A = {0, 1}. If F = {s | ∀ x1∈A, s={x1}} (the family you chose), then you'll have F = ∅, and it will not be the case that the union of F will be A. If you change your definition slightly, you'll get F = {{0}, {1}}, and then it will be the case that the union of F is equal to A.

[Daniil Zhitov]

Yes, I have already understood my mistake and have solved the level by changing the universal quantifier to the existential one.

[awefhio]

I am currently working through the Set theory game on Level 6 / 8 : A subset of a union intersected with the complement of another

image.png

I have no issues unwrapping h and the goal with the given proofs, but I'm not sure how to use h1 at all given this relatively complicated statement. Any pointers as to how to break h1 down into a more usable form?

[Mario Carneiro]

h says that $x\in y$ for some $y\in F$, and it suffices to show that $y\in G$ as well. What happens if $y\notin G$?

[awefhio]

How would I try to introduce this idea?

Something like

have hGc : x ∈ (⋃₀ G)ᶜ

or

have hy : y ∈ Gᶜ

would not work since I'll have to prove the statements first.

[Dan Velleman]

You can use have to assert something that you haven't proven yet. Proving that statement becomes your immediate goal. Once you have proven the statement, you return to your original goal, with the statement asserted by the have available as a new assumption.

[Dan Velleman]

In the set theory game, click on have in the list of tactics on the right and look at the first bullet point.

[awefhio]

Dan Velleman said:

You can use have to assert something that you haven't proven yet. Proving that statement becomes your immediate goal. Once you have proven the statement, you return to your original goal, with the statement asserted by the have available as a new assumption.

I think I do understand this part. The issue I'm having is what do I do after introducing the "have" statement.

[awefhio]

Mario Carneiro said:

h says that $x\in y$ for some $y\in F$, and it suffices to show that $y\in G$ as well. What happens if $y\notin G$?

Oh I think I know, I assert  $y\in G$ then I try proving by contradiction?

[awefhio]

I got it, thanks!!

[Matthew Khoriaty]

image.png
Why did it give me False instead of "¬t ∈ G", which I could then use to prove the goal. I don't see any contradictions in the assumptions themselves.

Edit: Turned out it gave me another goal. Case 1 had assumption "false" and Case 2 had "not t in G". That makes sense.

[Notification Bot]

A message was moved here from #lean4 > simp(rocs) with state by Kyle Miller.

[Dan Velleman]

An alternative way to proceed for this proof: To prove the goal t ∈ F ∧ t ∈ Gᶜ, you have to prove both t ∈ F and t ∈ Gᶜ. The first is easy, because you have it as an assumption. I would prove the second by contradiction: assume t ∈ G and then use your assumption right to get a contradiction. (Note that ∀ t ∈ G, x ∉ t is shorthand for ∀ t, t ∈ G → x ∉ t.)