levels.

server/testgame/TestGame.lean

@@ -7,18 +7,24 @@ import TestGame.Levels.Contradiction
 --import TestGame.Levels.Prime
 import TestGame.Levels.Induction
 
-Game "TestGame"
+import TestGame.Levels.LeanStuff
+import TestGame.Levels.SetTheory
+import TestGame.Levels.Function
+import TestGame.Levels.SetFunction
 
-Title "Lean 4 game"
 
+
+Game "TestGame"
+Title "Lean 4 game"
 Introduction
 "Work in progress.
 "
-
 Conclusion
 "There is nothing else so far. Thanks for rescuing natural numbers!"
 
 
-Path Proposition → Implication → Predicate → Contradiction
+Path Proposition → Implication → Predicate → Contradiction → LeanStuff
 --Path Predicate → Prime
-Path Predicate → Induction
+Path Predicate → Induction → LeanStuff → Function → SetFunction
+
+Path LeanStuff → SetTheory → SetFunction

server/testgame/TestGame/Levels/Contradiction.lean

@@ -6,5 +6,5 @@ import TestGame.Levels.Contradiction.L05_Contrapose
 import TestGame.Levels.Contradiction.L06_Summary
 
 Game "TestGame"
-World "Predicate"
+World "Contradiction"
 Title "Widerspruch"

server/testgame/TestGame/Levels/Function.lean

@@ -0,0 +1,5 @@
+import TestGame.Levels.Function.L01_xxx
+
+Game "TestGame"
+World "Function"
+Title "Abbildungen"

server/testgame/TestGame/Levels/Function/L01_xxx.lean

@@ -0,0 +1,26 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Function"
+Level 1
+
+Title "Abbildungen"
+
+Introduction
+"
+In diesem Kapitel lernen wir mit Abbildungen/Funktionen umzugehen.
+
+Funktionen auf `ℕ`.
+
+"
+
+Statement
+    "TODO"
+    : True := by
+  trivial
+
+Tactics rw

server/testgame/TestGame/Levels/LeanStuff.lean

@@ -0,0 +1,5 @@
+import TestGame.Levels.LeanStuff.L01_xxx
+
+Game "TestGame"
+World "LeanStuff"
+Title "Lean"

server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean

@@ -0,0 +1,32 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "LeanStuff"
+Level 1
+
+Title ""
+
+Introduction
+"
+Dieses Kapitel führt ein paar Lean-spezifische Sachen ein, die du wissen solltest.
+
+Mathematisch haben diese Sachen keinen Inhalt, aber es ist wichtig, dass du etwas
+verstehst wie Lean manche Sachen macht.
+
+
+- Implizite und explizite Argumente.
+- Types
+
+"
+
+open Set
+
+Statement
+    "TODO" : True := by
+  trivial
+
+Tactics rw

server/testgame/TestGame/Levels/SetFunction.lean

@@ -0,0 +1,5 @@
+import TestGame.Levels.SetFunction.L01_xxx
+
+Game "TestGame"
+World "SetFunction"
+Title "Abbildungen 2"

server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean

@@ -0,0 +1,24 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetFunction"
+Level 1
+
+Title "Abbildungen"
+
+Introduction
+"
+Fortsetzung: Funktionen auf Mengen.
+
+"
+
+Statement
+    "TODO"
+    : True := by
+  trivial
+
+Tactics rw

server/testgame/TestGame/Levels/SetTheory.lean

@@ -0,0 +1,5 @@
+import TestGame.Levels.SetTheory.T01_Set
+
+Game "TestGame"
+World "SetTheory"
+Title "Mengenlehre"

server/testgame/TestGame/Levels/SetTheory/T01_Set.lean

@@ -0,0 +1,47 @@
+import TestGame.Metadata
+
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "SetTheory"
+Level 1
+
+Title "Mengen"
+
+Introduction
+"
+In diesem Kapitel schauen wir uns Mengen an.
+
+Zuerst ein ganz wichtiger Punkt: Alle Mengen in Lean sind homogen. Das heisst,
+alle Elemente in einer Menge haben den gleichen Typ.
+
+Zum Beispiel `{1, 4, 6}` ist eine Menge von natürlichen Zahlen. Aber man kann keine
+Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` definieren, da die Elemente unterschiedliche Typen haben.
+
+Für einen Typen `{X : Type*}` definiert damit also `set X` der Type aller Mengen mit Elementen aus
+`X`.  `set.univ` ist dann ganz `X` also Menge betrachtet, und es ist wichtig den Unterschied
+zu kennen: `(univ : set X)` und `(X : Typ*)` haben nicht den gleichen Typ und sind damit auch nicht
+austauschbar!
+
+Am anderen Ende sitzt die leere Menge `(∅ : set X)` (`\\empty`). Bei `univ` und `∅` versucht Lean
+automatisch den Typ zu erraten, in exotischen Beispielen muss man wie oben diesen explizit angeben.
+
+Als erste Operationen schauen wir uns `∪` (`\\union` oder `\\cup`), `∩`
+(`\\inter` oder `\\cap`) und `\\` (`\\\\` oder `\\ `)
+
+"
+
+open Set
+
+Statement
+    "Wenn $B$ wahr ist, dann ist die Implikation $A \\Rightarrow (A ∧ B)$ wahr."
+    {X : Type _} {A B : Set X} : univ \ (A ∩ B) ∪ ∅ = (univ \ A) ∪ (univ \ B) ∪ (A \ B) := by
+  rw [Set.diff_inter]
+  rw [Set.union_empty]
+  rw [Set.union_assoc]
+  rw [←Set.union_diff_distrib]
+  rw [Set.univ_union]
+
+Tactics rw