Intersection of a families of sets

Stream: new members

[Yagub Aliyev]

If I have assumptions:
hA: x ∈ A
hB: x ∈ B
How do I prove my goal?
∀ S ∈ {A, B}, x ∈ S

[Kevin Buzzard]

You should eat l read about #backticks to make your question look nicer and you should read about #mwe to make your question easier for others to answer. Right now it's ambiguous because it's not possible to determine the types of your terms from the data you've given us.

[Yagub Aliyev]

Like this?
U: Type
AB: Set U
x: U
S: Set U
Assumptions:
hA: x ∈ A
hB: x ∈ B
Goal:
S ∈ {A, B} → x ∈ S

[Yagub Aliyev]

U: Type
AB: Set U
x: U
S: Set U
hA: x ∈ A
hB: x ∈ B
S ∈ {A, B} → x ∈ S

[Riccardo Brasca]

You should write the full statement of what you want to prove. The idea is that people can just copy/paste your code in VS code and have a look, without getting any error (so be sure to include all the imports and so on)

[Yagub Aliyev]

[like] Yagub Aliyev reacted to your message:

[Dan Velleman]

It looks to me like you're playing the set theory game.

In your first message, you listed the goal as ∀ S ∈ {A, B}, x ∈ S. If that's your goal, then since it starts with ∀ S, a good first step would be to introduce an arbitrary S by using the tactic intro S. But it looks like you may have done that, because in your next message you have S : Set U in the context and now your goal is listed as S ∈ {A, B} → x ∈ S. But once again, the form of the goal suggests what your next step should be. Since your goal is an if-then statement, a good next step would be to introduce the assumption S ∈ {A, B}, once again using the intro tactic.

The hints in the set theory game also tell you about a theorem you can use to write out the meaning of S ∈ {A, B}.

[Yagub Aliyev]

Yes, I am copying from NNG (Natural Number Game) and Set theory game where not all code is given. I will try to learn the details of VS codes after I am done with these 2 games. Thank you for the support.

[Kevin Buzzard]

Yagub Aliyev said:

Yes, I am copying from NNG (Natural Number Game) and Set theory game where not all code is given. I will try to learn the details of VS codes after I am done with these 2 games. Thank you for the support.

In which case, can you post the URL of the level you're asking about?

[Dan Velleman]

Note that in these games, there are restrictions on what tactics you can use. As you go through the game, tactics are unlocked, and at any level of the game, you can only use tactics that have been unlocked at that point in the game. That's why it's helpful to specify what level of the game you're working on. If you just post a general question without saying what game level you're working on, people are likely to give answers that won't work in the game, because they involve tactics that are not available at that point in the game.

[Yagub Aliyev]

Dan Velleman said:

Note that in these games, there are restrictions on what tactics you can use. As you go through the game, tactics are unlocked, and at any level of the game, you can only use tactics that have been unlocked at that point in the game. That's why it's helpful to specify what level of the game you're working on. If you just post a general question without saying what game level you're working on, people are likely to give answers that won't work in the game, because they involve tactics that are not available at that point in the game.

I didn't face this problem in Set Theory Game. It accepts even very advanced tactics not in the list of unlocked ones. But I do sometimes try several tactics for the same task recommended by you even after solving it to understand better how they work.

[Dan Velleman]

There are a few tactics (such as constructor, rw, left, and right) that are mentioned in the hints in the set theory game as alternative ways to solve some of the levels. Those tactics are then available, even though they are not listed as being unlocked. But other tactics should not be available in the game. When I try to use a tactic in the game that is not unlocked, I get an error message. I'm not sure why that isn't happening to you.

[Yagub Aliyev]

Dan Velleman said:

There are a few tactics (such as constructor, rw, left, and right) that are mentioned in the hints in the set theory game as alternative ways to solve some of the levels. Those tactics are then available, even though they are not listed as being unlocked. But other tactics should not be available in the game. When I try to use a tactic in the game that is not unlocked, I get an error message. I'm not sure why that isn't happening to you.

I tried some unusual commands like "propext", "tauto" etc. without any issues, even though they are not on the wall. I suppose after a certain level of the game the restrictions are lifted. Is that right? By the way "tauto" seems to be kind of cheating at this level :-)

[Dan Velleman]

When I try to use tauto in the set theory game, I get an error message saying that tauto has not been unlocked. I don't know why you were able to use it. This sounds like a bug in the game software.

[Kevin Buzzard]

In NNG There are several options available for how to play the game available by a switch at the beginning. These control how much tactic abuse you can get away with

[Kevin Buzzard]

Rules: regular, relaxed or none. It's also there in the set theory game

[Dan Velleman]

Thanks Kevin, that might explain it. It looks like the different settings are:

• regular: You can't use tactics that haven't been unlocked.
• relaxed: You can use tactics that haven't been unlocked, but you get a warning.
• none: You can use any tactic with no warnings.

[Samuel Levi Schmidt]

Dan Velleman said:

When I try to use tauto in the set theory game, I get an error message saying that tauto has not been unlocked. I don't know why you were able to use it. This sounds like a bug in the game software.

There was a bug, but but should be fixed by now as far as I can tell (see also https://github.com/djvelleman/STG4/issues/6#issue-2079010666

[Yagub Aliyev]

Dan Velleman said:

Thanks Kevin, that might explain it. It looks like the different settings are:

• regular: You can't use tactics that haven't been unlocked.
• relaxed: You can use tactics that haven't been unlocked, but you get a warning.
• none: You can use any tactic with no warnings.

Yes, I switched to "none" option in NNG from the beginning. I like to try different ways of solving the tasks.