search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

Potenzmenge lacks the theorem `Set.union_comm` #37

Open bernborgess opened 3 months ago

bernborgess commented 3 months ago

Since it is still under development, I am not sure if every path is properly defined, but here is what I found.

In the level 2 / 8 of [WIP] Mengenlehre 2 we are introduced to theorems involving Powerset and subset_union. Even so, we are not allowed to close a goal with Set.subset_union_of_subset_left, when we cannot use commutativity of the union:

image

Is this the intention? My proof so far:

example (X Y : Set ℕ): 𝒫 X ∪ 𝒫 Y ⊆ 𝒫 (X ∪ Y) := by
  intro S
  intro sInPxPy
  rw [Set.mem_powerset_iff]
  rw [Set.mem_union] at sInPxPy
  rcases sInPxPy with spx | spy
  rw [Set.mem_powerset_iff] at spx
  apply Set.subset_union_of_subset_left spx Y
  rw [Set.mem_powerset_iff] at spy
  have h : S ⊆ Y ∪ X
  apply Set.subset_union_of_subset_left spy X

Shouldn't Set.union_comm be available?

joneugster commented 3 months ago

Thanks! Even though the Set Theory stuff needs refactoring, your sample proof might come in helpful. So I'll leave this open for the time being