add Image/Preimage planet

.i18n/de/Game.pot

@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.7.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Tue Sep  3 15:32:52 2024\n"
+"POT-Creation-Date: Thu Sep  5 10:36:56 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: de\n"
@@ -5017,31 +5017,6 @@ msgid "**Robo**: Siehst du die Annahme `«{hs}» : f ∘ g = succ ∘ f`?\n"
 "`f₁ = f₂` in `∀ x, f₁ x = f₂ x` um."
 msgstr ""
 
-#: Game.Levels.FunctionSurj.L13_SurjectiveRange
-msgid "Range of Surjection"
-msgstr ""
-
-#: Game.Levels.FunctionSurj.L13_SurjectiveRange
-msgid "The range of a function is the set of all outputs.\n"
-"\n"
-"In this level you show that a function is surjective if and only if the range of\n"
-"the function is equal to the universal subset of the codomain. For `f : A → B`,\n"
-"the range of `f` is defined as\n"
-"\n"
-"```\n"
-"range f : Set B := {b | ∃ a, f a = b}\n"
-"```"
-msgstr ""
-
-#: Game.Levels.FunctionSurj.L13_SurjectiveRange
-msgid "**Du**: Wie zeigt man denn schon wieder Gleichheit von Mengen?"
-msgstr ""
-
-#: Game.Levels.FunctionSurj.L13_SurjectiveRange
-msgid "**Robo**: Ich habe ein relevantes Resultat gefunden: `mem_range`.\n"
-"Such das mal in denem Inventar!"
-msgstr ""
-
 #: Game.Levels.FunctionSurj.L14_choose
 msgid "Every function with nonempty fibres has a right inverse."
 msgstr ""
@@ -5176,15 +5151,6 @@ msgid "Als ihr das Problem gelöst habt, erschleicht euch ein starkes\n"
 "Also geht ihr zurück und nehmt die rechte Gabelung."
 msgstr ""
 
-#: Game.Levels.FunctionInj.L03_InjectiveRange
-msgid "Range of Injective"
-msgstr ""
-
-#: Game.Levels.FunctionInj.L03_InjectiveRange
-msgid "For an injective function `f : A → B` the fibres of the elements in the range\n"
-"are singletons."
-msgstr ""
-
 #: Game.Levels.FunctionInj.L04_Injective
 msgid "Monotone Funktionen"
 msgstr ""
@@ -5286,26 +5252,6 @@ msgstr ""
 msgid ""
 msgstr ""
 
-#: Game.Levels.FunctionInj.L08_LeftInvPreimage
-msgid "Preimage of the inverse"
-msgstr ""
-
-#: Game.Levels.FunctionInj.L08_LeftInvPreimage
-msgid "The image of a set `S : Set A` along a  function `f : A → B` is the set of all elements\n"
-"`b : B` that are the image of some element `a : A` in `S`. We denote it by `f '' S` and\n"
-"define it as below.\n"
-"```\n"
-"f '' S = {b : B | ∃ a : A, a ∈ S ∧ f a = b}\n"
-"```\n"
-"\n"
-"Note that an element of the image is a triple `⟨b, a, h⟩` where `b` is the image of `a` and `h`\n"
-"is the proof that `a` is in `S` and `f a = b`.\n"
-"\n"
-"The image of function with a left in\n"
-"verse is a subset of the preimage of the inverse of\n"
-"the same subset."
-msgstr ""
-
 #: Game.Levels.FunctionInj.L09_InjOfHasLeftInv
 msgid "Functions with left inverses are injective."
 msgstr ""
@@ -5323,11 +5269,11 @@ msgid ""
 msgstr ""
 
 #: Game.Levels.FunctionInj.L11_InjHasLeftInv
-msgid "Injections with nonempty domain have retract."
+msgid "Injections have a left inverse, and vice versa"
 msgstr ""
 
 #: Game.Levels.FunctionInj.L11_InjHasLeftInv
-msgid "In this level you show that an injective function with a nonempty domain has a left inverse."
+msgid ""
 msgstr ""
 
 #: Game.Levels.FunctionInj
@@ -5496,11 +5442,74 @@ msgstr ""
 msgid "In this level, you will prove that the the diagonal function is injective."
 msgstr ""
 
-#: Game.Levels.FunctionBij.L09_Preimage_Injective
+#: Game.Levels.FunctionBij
+msgid "Bijektivität"
+msgstr ""
+
+#: Game.Levels.FunctionBij
+msgid "Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf\n"
+"eine Insel komplett mit Wasser bedeckt zu sein scheint.\n"
+"\n"
+"Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,\n"
+"vereinzelte aus Lehm.\n"
+"\n"
+"Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt."
+msgstr ""
+
+#: Game.Levels.FunctionImage.L01_ImagePreimage
+msgid "Bild/Urbild"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L01_ImagePreimage
+msgid "`f '' S` ist das Bild,\n"
+"`f ⁻¹' V` das Urbild,\n"
+"\n"
+"`f '' S := {f a | a ∈ S}`\n"
+"`f ⁻¹' V := {a | f a ∈ V}`"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L01_ImagePreimage
+msgid ""
+msgstr ""
+
+#: Game.Levels.FunctionImage.L02_ImagePreimage
+msgid ""
+msgstr ""
+
+#: Game.Levels.FunctionImage.L03_InjectiveRange
+msgid "Range of Injective"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L03_InjectiveRange
+msgid "For an injective function `f : A → B` the fibres of the elements in the range\n"
+"are singletons."
+msgstr ""
+
+#: Game.Levels.FunctionImage.L04_LeftInvPreimage
+msgid "Preimage of the inverse"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L04_LeftInvPreimage
+msgid "The image of a set `S : Set A` along a  function `f : A → B` is the set of all elements\n"
+"`b : B` that are the image of some element `a : A` in `S`. We denote it by `f '' S` and\n"
+"define it as below.\n"
+"```\n"
+"f '' S = {b : B | ∃ a : A, a ∈ S ∧ f a = b}\n"
+"```\n"
+"\n"
+"Note that an element of the image is a triple `⟨b, a, h⟩` where `b` is the image of `a` and `h`\n"
+"is the proof that `a` is in `S` and `f a = b`.\n"
+"\n"
+"The image of function with a left in\n"
+"verse is a subset of the preimage of the inverse of\n"
+"the same subset."
+msgstr ""
+
+#: Game.Levels.FunctionImage.L05_Preimage_Injective
 msgid "Preimage of surjective is injective"
 msgstr ""
 
-#: Game.Levels.FunctionBij.L09_Preimage_Injective
+#: Game.Levels.FunctionImage.L05_Preimage_Injective
 msgid "Given a function `f : A → B` we obtain a function `preimage f : Set B → Set A`\n"
 "by taking the preimage of sets of `B`. Recall that\n"
 "```\n"
@@ -5510,22 +5519,37 @@ msgid "Given a function `f : A → B` we obtain a function `preimage f : Set B 
 "Show that `preimage f` is injective iff f is surjective."
 msgstr ""
 
-#: Game.Levels.FunctionBij.L09_Preimage_Injective
+#: Game.Levels.FunctionImage.L05_Preimage_Injective
 msgid "Now `change (f ⁻¹' {«{y}»}).Nonempty`"
 msgstr ""
 
-#: Game.Levels.FunctionBij
-msgid "Bijektivität"
+#: Game.Levels.FunctionImage.L06_SurjectiveRange
+msgid "Range of Surjection"
 msgstr ""
 
-#: Game.Levels.FunctionBij
-msgid "Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf\n"
-"eine Insel komplett mit Wasser bedeckt zu sein scheint.\n"
+#: Game.Levels.FunctionImage.L06_SurjectiveRange
+msgid "The range of a function is the set of all outputs.\n"
 "\n"
-"Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,\n"
-"vereinzelte aus Lehm.\n"
+"In this level you show that a function is surjective if and only if the range of\n"
+"the function is equal to the universal subset of the codomain. For `f : A → B`,\n"
+"the range of `f` is defined as\n"
 "\n"
-"Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt."
+"```\n"
+"range f : Set B := {b | ∃ a, f a = b}\n"
+"```"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L06_SurjectiveRange
+msgid "**Du**: Wie zeigt man denn schon wieder Gleichheit von Mengen?"
+msgstr ""
+
+#: Game.Levels.FunctionImage.L06_SurjectiveRange
+msgid "**Robo**: Ich habe ein relevantes Resultat gefunden: `mem_range`.\n"
+"Such das mal in denem Inventar!"
+msgstr ""
+
+#: Game.Levels.FunctionImage
+msgid "Injektivität"
 msgstr ""
 
 #: Game

Game.lean

@@ -18,6 +18,7 @@ import Game.Levels.NewStuff.Prime
 import Game.Levels.FunctionSurj
 import Game.Levels.FunctionInj
 import Game.Levels.FunctionBij
+import Game.Levels.FunctionImage
 -- import Game.Levels.SetTheory
 
 -- *uncomment the following line to get the incomplete planets.*

Game/Levels/FunctionBij.lean

@@ -6,7 +6,6 @@ import Game.Levels.FunctionBij.L05_BijectionEquivalence
 import Game.Levels.FunctionBij.L06_CurryEquiv
 import Game.Levels.FunctionBij.L07_CurrySurjective
 import Game.Levels.FunctionBij.L08_Diagonal
-import Game.Levels.FunctionBij.L09_Preimage_Injective
 
 World "FunctionBij"
 Title "Bijektivität"

Game/Levels/FunctionImage.lean

@@ -0,0 +1,9 @@
+import Game.Levels.FunctionImage.L01_ImagePreimage
+import Game.Levels.FunctionImage.L02_ImagePreimage
+import Game.Levels.FunctionImage.L03_InjectiveRange
+import Game.Levels.FunctionImage.L04_LeftInvPreimage
+import Game.Levels.FunctionImage.L05_Preimage_Injective
+import Game.Levels.FunctionImage.L06_SurjectiveRange
+
+World "FunctionImage"
+Title "Image/Preimage"

Game/Levels/FunctionImage/L01_ImagePreimage.lean

@@ -0,0 +1,34 @@
+import Game.Metadata
+
+open Function Set
+
+World "FunctionImage"
+Level 1
+Title "Bild/Urbild"
+
+Introduction "
+`f '' S` ist das Bild,
+`f ⁻¹' V` das Urbild,
+
+`f '' S := {f a | a ∈ S}`
+`f ⁻¹' V := {a | f a ∈ V}`
+"
+
+/--  -/
+TheoremDoc Set.image_preimage_subset as "image_preimage_subset" in "Set"
+
+-- Set theory
+example {x : Nat} (h : x ∈ {a : ℕ | Even a}) : False := by
+  obtain ⟨⟩ := h
+  sorry
+
+Statement Set.image_preimage_subset {A B : Type} (f : A → B) (S : Set B) :
+f '' (f ⁻¹' S) ⊆ S := by
+  intro b
+  intro hb
+  simp at hb
+  obtain ⟨a, ha₁, ha₂⟩ := hb
+  rw [ha₂] at ha₁
+  assumption
+
+NewDefinition Set.image Set.preimage

Game/Levels/FunctionImage/L02_ImagePreimage.lean

@@ -0,0 +1,22 @@
+import Game.Metadata
+
+
+World "FunctionImage"
+Level 2
+Title ""
+
+open Function Set
+
+Statement {A B : Type} {f : A → B} (hf : Surjective f) (s : Set B) :
+f '' (f ⁻¹' s) = s := by
+  ext b
+  simp
+  constructor
+  · apply image_preimage_subset -- Lvl 1
+  · intro hb
+    obtain ⟨a, ha⟩ := hf b
+    use a
+    constructor
+    · rw [ha]
+      assumption
+    · assumption

Game/Levels/FunctionInj/L03_InjectiveRange.lean → Game/Levels/FunctionImage/L03_InjectiveRange.lean

@@ -1,7 +1,6 @@
 import Game.Metadata
 
-
-World "FunctionInj"
+World "FunctionImage"
 Level 3
 
 Title "Range of Injective"
@@ -27,3 +26,5 @@ Statement Injective.exists_unique_of_mem_range {A B : Type} {f : A → B} (hf :
   · intro a' ha'
     apply hf
     rw [ha',ha]
+
+NewDefinition Set.Range

Game/Levels/FunctionInj/L08_LeftInvPreimage.lean → Game/Levels/FunctionImage/L04_LeftInvPreimage.lean

@@ -1,8 +1,8 @@
 import Game.Metadata
 
 
-World "FunctionInj"
-Level 8
+World "FunctionImage"
+Level 4
 
 Title "Preimage of the inverse"
 

Game/Levels/FunctionBij/L09_Preimage_Injective.lean → Game/Levels/FunctionImage/L05_Preimage_Injective.lean

@@ -1,8 +1,8 @@
 import Game.Metadata
 
 
-World "FunctionBij"
-Level 9
+World "FunctionImage"
+Level 5
 
 Title "Preimage of surjective is injective"
 

Game/Levels/FunctionSurj/L13_SurjectiveRange.lean → Game/Levels/FunctionImage/L06_SurjectiveRange.lean

@@ -1,8 +1,8 @@
 import Game.Metadata
 
 
-World "FunctionSurj"
-Level 13
+World "FunctionImage"
+Level 6
 
 Title "Range of Surjection"
 

Game/Levels/FunctionImage/LXX_Set6.lean

@@ -0,0 +1,15 @@
+import Game.Metadata
+
+open Set
+
+-- DELETE?
+
+example (f : ℝ → ℝ) (hfib : ncard (f ⁻¹' {0}) = 2) : ∃ (x₁ x₂ : ℝ ), x₁ ≠ x₂ ∧ f x₁ = 0 ∧ f x₂ = 0 := by
+  apply ncard_eq_two.mp at hfib
+  obtain ⟨ x₁, x₂, h_ne, h_fib_eq ⟩ := hfib
+  use x₁, x₂
+  constructor
+  assumption
+  change x₁ ∈ f ⁻¹' {0} ∧ x₂ ∈ f ⁻¹' {0}
+  rw [h_fib_eq]
+  tauto

Game/Levels/FunctionInj.lean

@@ -1,11 +1,9 @@
 import Game.Levels.FunctionInj.L01_Injective
 import Game.Levels.FunctionInj.L02_Injective
-import Game.Levels.FunctionInj.L03_InjectiveRange
 import Game.Levels.FunctionInj.L04_Injective
 import Game.Levels.FunctionInj.L05_Injective
 import Game.Levels.FunctionInj.L06_SuccHasLeftInv
 import Game.Levels.FunctionInj.L07_Extend
-import Game.Levels.FunctionInj.L08_LeftInvPreimage
 import Game.Levels.FunctionInj.L09_InjOfHasLeftInv
 import Game.Levels.FunctionInj.L10_RightInvOfLeftInv
 import Game.Levels.FunctionInj.L11_InjHasLeftInv

Game/Levels/FunctionInj/L04_Injective.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 4
+Level 3
 
 Title "Monotone Funktionen"
 

Game/Levels/FunctionInj/L05_Injective.lean

@@ -2,7 +2,7 @@ import Game.Metadata
 
 
 World "FunctionInj"
-Level 5
+Level 4
 
 Title "Monotone Funktionen"