|
|
import Adam.Metadata
|
|
|
import Mathlib
|
|
|
|
|
|
Game "Adam"
|
|
|
World "Function"
|
|
|
Level 1
|
|
|
|
|
|
Title "Anonyme Funktionen"
|
|
|
|
|
|
Introduction
|
|
|
"
|
|
|
Auf die Frage hin, ob sie von einem Bibliothek wisse, erzählt euch das kleine Mädchen,
|
|
|
dass es auf der Insel nur einen gäbe, aber sie bedrängt euch so mit einer Frage,
|
|
|
dass sie euch gar nicht sagt, wo dieser zu finden sei.
|
|
|
"
|
|
|
|
|
|
Statement "" : ∃ f : ℤ → ℤ, ∀ x, f x < x := by
|
|
|
use (fun x ↦ x - 1)
|
|
|
simp
|
|
|
|
|
|
Hint : ∃ f : ℤ → ℤ, ∀ x, f x < x =>
|
|
|
"
|
|
|
**Robo**: `f : ℤ → ℤ` ist die Notation für eine Funktion und `f x` ist diese Funktion
|
|
|
angewendet auf ein Element `(x : ℤ)`.
|
|
|
|
|
|
**Du**: War `→` nicht eben noch eine Implikation?
|
|
|
|
|
|
**Robo**: Doch, die brauchen das gleiche Zeichen für beides.
|
|
|
|
|
|
**Du**: Dann ist `f : ℤ → ℤ` also einfach abstrakt irgendeine Funktion,
|
|
|
wie definier ich aber jetzt konkret eine Abbildungsvorschrift?
|
|
|
|
|
|
**Robo**: Man kennt hier eine Notation für eine anonyme Funktion:
|
|
|
`fun (x : ℤ) ↦ x ^ 2` ist
|
|
|
|
|
|
$$
|
|
|
\\begin\{aligned}
|
|
|
f : \\mathbb\{ℤ} &\\to \\mathbb\{ℤ} \\\\
|
|
|
x &\\mapsto x ^ 2
|
|
|
\\end\{aligned}
|
|
|
$$
|
|
|
|
|
|
**Robo**: PS, `↦` ist `\\mapsto`. Aber man kann auch stattdessen `=>` benützen.
|
|
|
"
|
|
|
|
|
|
HiddenHint : ∃ f : ℕ → ℤ, ∀ x, f x < x =>
|
|
|
"
|
|
|
**Du**: Ja aber was mach ich damit?
|
|
|
|
|
|
**Robo**: Wie immer gehst du ein `∃` mit `use …` an.
|
|
|
"
|
|
|
|
|
|
-- TODO: Why does this not show?
|
|
|
HiddenHint : ∀ (x : ℤ), (fun (y : ℤ) => y - 1) x < x =>
|
|
|
"**Du**: Zu was sich das wohl vereinfacht?"
|
|
|
|
|
|
HiddenHint (x : ℤ) : (fun y => y - 1) x < x =>
|
|
|
"**Du**: Zu was sich das wohl vereinfacht?"
|
|
|
|
|
|
Conclusion "Das Mädchen wird kurz ruhig, dann beginnt es zu lächeln und zeigt strahlend
|
|
|
in eine Richtung. Ihr folgt ihrem Finger und euch fällt in weiter ferne eine pompöse Struktur
|
|
|
auf einem flachen Hügel auf.
|
|
|
"
|