diff --git a/.i18n/en/Game.pot b/.i18n/en/Game.pot index d59643a..e23fa6b 100644 --- a/.i18n/en/Game.pot +++ b/.i18n/en/Game.pot @@ -1,7 +1,7 @@ msgid "" msgstr "Project-Id-Version: Game v4.21.0\n" "Report-Msgid-Bugs-To: \n" -"POT-Creation-Date: 2026-03-26\n" +"POT-Creation-Date: 2026-04-30\n" "Last-Translator: \n" "Language-Team: none\n" "Language: en\n" @@ -173,6 +173,17 @@ msgid "## Summary\n" "- `use a * a + 1`" msgstr "" +#: Game.Levels.TutorialWorld.Level01 +msgid "Most levels in this game will require you to prove a mathematical theorem. In the middle of the\n" +"screen, you will see your \"Active Goal\", which includes \"Objects:\" `x: ℝ` and a \"Goal\" `x=x`.\n" +"In later levels, you may also get a \"Assumptions\" line. Your objects and assumptions are what you\n" +"have to work with. In this case, we know that `x` is in `ℝ`, which means `x` is a real number.\n" +"From this, we have to prove our goal, that `x=x`.\n" +"\n" +"The first tactic we will use is the `rfl` tactic. `rfl` stands for \"reflexivity\". `rfl` will solve\n" +"goals when the left side of an equation is the same as the right side, at least up to definitions." +msgstr "" + #: Game.Levels.LinearIndependenceSpanWorld.Level03 msgid "`subset_trans` is a proof that subsets are transitive. The syntax is that if you have `h1 : A ⊆ B`\n" "and `h2 : B ⊆ C`, then `subset_trans h1 h2` is a proof that `A ⊆ C`." @@ -215,23 +226,6 @@ msgid "`Complex.ext` allows you to split complex numbers into their real and ima "and the other `a.im = b.im`." msgstr "" -#: Game.Levels.LinearMapsWorld.Level04 -msgid "Now let's prove a fundamental property that every linear map must satisfy: they always map the zero vector to the zero vector.\n" -"\n" -"## The Key Insight\n" -"\n" -"This might seem obvious, but it's an important consequence of linearity that we'll use in many future proofs.\n" -"\n" -"## Why This Matters\n" -"\n" -"The fact that linear maps preserve zero is often the first step in proving that the null space is non-empty, and it's crucial for understanding the structure of linear maps.\n" -"\n" -"### Your Goal\n" -"Prove that for any linear map T, we have T(0) = 0.\n" -"\n" -"**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." -msgstr "" - #: Game.Levels.InnerProductWorld.Level01 msgid "For any vector `v`, `⟪v, v⟫ = 0` if and only if `v` is the zero vector.\n" "\n" @@ -470,17 +464,20 @@ msgstr "" msgid "The `constructor` tactic" msgstr "" -#: Game.Levels.TutorialWorld.Level05 -msgid "## Summary\n" -"\n" -"If we have some object or function with some definition, `unfold object` will rewrite the object\n" -"with its definition everywhere. Lean often unfolds terms automatically, but some tactics and definitions\n" -"are not unfolded automatically. The `unfold` tactic also helps make it easier to take the next steps.\n" +#: Game.Levels.TutorialWorld.Level10 +msgid "The `induction` tactic is a powerful tool to help you to prove statements involving natural numbers.\n" +"It splits a proof into two cases: a base case and an inductive step. The base case is the smallest\n" +"natural number you need to prove the proof for. The inductive step proves the theorem for all other\n" +"numbers. In the inductive step, you can assume the theorem holds for some value `n`, and must then\n" +"prove that it holds for `n + 1`, also written as `Nat.succ n`, the successor of `n`. Induction can\n" +"also be used to prove theorems about objects indexed by natural numbers, such as vectors whose\n" +"dimension can be described by a natural number.\n" "\n" -"## Example:\n" +"The syntax for the `induction` tactic in Lean 4 is `induction n with | zero => ... | succ n h => ...`.\n" +"As long as `n` is an arbitrary natural number in the proof, this will do induction on `n`, where\n" +"`zero` handles the base case, `succ n` is the successor case, and `h` is the induction hypothesis.\n" "\n" -"If you have a goal `(P → Q) → (¬ Q → ¬ P)`, with `¬ P` (\\\"Not\\\" P) being defined as `P → False`,\n" -"using `unfold Not` will change the goal to `(P → Q) → ((Q → False) → (P → False))`" +"**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." msgstr "" #: Game.Levels.VectorSpaceWorld.Level04 @@ -622,41 +619,6 @@ msgid "Welcome to the **crown jewel** of linear map theory: the **Fundamental Th "**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." msgstr "" -#: Game.Levels.LinearIndependenceSpanWorld.Level01 -msgid "The first level of this world will introduce the definition of a linear combination. Let's\n" -"say we want to express that some vector `x` is a linear combination of some set `S ⊆ V`. This means\n" -"that there is some number of elements in `S`, that after some scalar multiplication, sums to `x`.\n" -"Since infinite sums are difficult (and sometimes impossible) to work with, we can't simply sum over\n" -"all of `S`. Instead, we take some smaller subset `s : Finset V`, with `↑s ⊆ S`, and sum over that.\n" -"Note here the `↑` character. This simply takes our finite set `s`, which is a `Finset`, and treats it\n" -"as a `Set`.\n" -"\n" -"Once we have the set we are summing over `s`, we need to also multiply the elements of `s` by scalars.\n" -"We do this with a function `f : V → K`, where each element of `s` gets mapped to the scalar we multiply by.\n" -"Now, we are able to understand the definition of linear combinations:\n" -"\n" -"```\n" -"def is_linear_combination (S : Set V) (x : V) : Prop :=\n" -" ∃ (s : Finset V) (f : V → K), (↑s ⊆ S) ∧ (x = Finset.sum s (fun v => f v • v))\n" -"```\n" -"\n" -"### The Goal\n" -"The goal of this level is to prove that if `v ∈ S`, then `v` is a linear combination of `s`. This can\n" -"be done simply by summing over the set `{v}`, with only multiplying by the scalar 1.\n" -"\n" -"### Defining functions\n" -"In this level, we need to use the `use` tactic to specify a function `f`. A very versatile way of doing\n" -"this is with the `fun` keyword. This allows you to write the function, and for Lean to accept it as a function.\n" -"For example, to write `f(x) = x²`, we can say `fun x => x * x`.\n" -"\n" -"### The return of the `simp` tactic\n" -"Since the levels in this world will become more difficult than in the last world, you are again allowed\n" -"to use the `simp` tactic. It is able to solve most simple equalities with vectors, and helps greatly\n" -"when trying to simplify properties of sets.\n" -"\n" -"**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." -msgstr "" - #: Game.Levels.TutorialWorld.Level10 msgid "## Summary\n" "You have now finished Tutorial World! Now, you can move on to Vector Space world.\n" @@ -672,20 +634,6 @@ msgstr "" msgid "In any vector space V over K, multiplying a vector by -1 gives its additive inverse." msgstr "" -#: Game.Levels.TutorialWorld.Level02 -msgid "The second tactic we will look at is the rewrite tactic. This tactic is how you \"substitute in\"\n" -"a value for something you know is equal. If you have an assumption `h: A=B`, and your goal is to\n" -"prove something about `A`, you can replace `A` with `B`, since they are equal.\n" -"\n" -"In this level, the goal is to prove `2 * y = 2 * (x + 7)`. You also have an assumption `h: y = x + 7`.\n" -"Writing `rw[h]` will rewrite `y` as `x + 7` in the goal.\n" -"\n" -"Also note that the `rw` tactic will automatically attempt the `rfl` tactic after it rewrites, so if\n" -"after the rewrite the goal is of the form `X = X`, it will automatically be solved.\n" -"\n" -"**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." -msgstr "" - #: Game.Levels.InnerProductWorld.Level03 msgid "The sum of two non-negative real numbers is non-negative." msgstr "" @@ -887,7 +835,7 @@ msgstr "" msgid "Challenge Level - Span After Removing Elements" msgstr "" -#: Game.Levels.LinearIndependenceSpanWorld.Level07 +#: Game.Levels.VectorSpaceWorld.Level05 msgid "`union_subset` is a proof that if `a ⊆ c` and `b ⊆ c`, then `a ∪ b ⊆ c`. This means that if you\n" "have two sets that are subsets of the same set, their union is also a subset of that set." msgstr "" @@ -1179,6 +1127,69 @@ msgstr "" msgid "Surjectivity means range equals codomain." msgstr "" +#: Game.Levels.LinearIndependenceSpanWorld.Level07 +msgid "This is the \"boss level\" of the Linear Independence and Span World. This level is a\n" +"proof that in a linearly independent set, linear combinations are unique. There are also a few new tactics\n" +"and multiple new theorems you should use.\n" +"\n" +"### The Goal\n" +"In this level, we have 5 objects and 6 hypotheses about those objects. We have the set `S : Set V`,\n" +"which is the linearly independent set we are working with. We also have `s` and `f`, which are the set\n" +"and function we are summing over to get the first linear combination, and `t` and `g` are the second\n" +"linear combination. We have `hs : linear_independent_v K V S`, which states that `S` is linearly independent,\n" +"`hs : ↑s ⊆ S` and `ht : ↑t ⊆ S`, which state that `s` and `t` are both in `S`, so are valid linear\n" +"combinations of `S`. We know `hf0 : ∀ v ∉ s, f v = 0` and a similar `hg0`, which state that both functions\n" +"are zero outside of their domain. This helps us prove `f = g`, since otherwise we wouldn't know what\n" +"the values of `f` and `g` would be outside of `s` and `t`. Lastly, we have `heq : Finset.sum s (fun v => f v • v) = Finset.sum t (fun v => g v • v)`,\n" +"which shows that the two linear combinations are equal. We then must pove that `f = g`\n" +"\n" +"**Note:** This level may experience a hint display issue where hints repeat. If you see the same hint multiple times, the level is still working correctly - just continue with your proof as normal.\n" +"\n" +"### The `specialize` tactic\n" +"The `specialize` tactic can be thought of as the opposite of `use`. While `use` helps specify a value\n" +"for a `∃` in the goal, `specialize` specifies a value for a `∀` in a hypothesis. For example, if you\n" +"have a hypothesis `h : ∀ v : V, v • 1 = v`, and you have a vector `x : V`, then `specialize h x` will\n" +"change `h` to `h : x • 1 = x`. `specialize` also works if `h` is an implication. If `h1 : P → Q` is a\n" +"hypothesis, and `h2 : P` is a proof of `P`, then `specialize h1 h2` will change `h2` to `h2 : Q`.\n" +"\n" +"### The `by_cases` tactic\n" +"The `by_cases` tactic helps you prove something by cases. If you want to prove a statement about vectors\n" +"in `V`, but you want to split into cases where `v = 0` or `v ≠ 0`, `by_cases hv : v = 0` will split the\n" +"goal into two subgoals: one where you have a hypothesis `hv : v = 0`, and another where you have a hpyothesis\n" +"`hv : v ≠ 0`.\n" +"\n" +"### The `funext` tactic\n" +"The `funext` tactic lets you prove statements about functions. It works similarly to the `intro` tactic,\n" +"where you introduce an arbitrary object, but instead of introducing from a `∀` statement, it works if\n" +"you have a goal of the form `f = g`, where `funext x` will change the goal to the form `f x = g x`, and\n" +"give you an arbitrary `x` in the domain of `f` and `g`.\n" +"\n" +"### New theorems\n" +"This level requires multiple new theorems, particularly ones about Finsets and sums. There are two theorems\n" +"about vector spaces that can be proven quite easily, but they are still nice to have without needing\n" +"to prove them first. Instead of explaining them all here, you can look at them on the right side of\n" +"the screen. The new theorems are: `coe_union`, `union_subset`, `sub_smul`, `sum_add_distrib`, `sum_sub_distrib`,\n" +"`subset_union_left`, `subset_union_right`, `sum_subset`, `sub_eq_zero`, and `notMem_union`.\n" +"If you need more theorems, you can either prove them in lemmas, or if you want, you can go to the world\n" +"select menu and turn \"Rules\" to \"none\", which should allow you to use any tactic or theorem in Lean.\n" +"\n" +"### Proof overview\n" +"If you look at the hypotheses you have, the most important ones are that S is linearly independent and\n" +"that the two sums are equal. When you have a statement that a set is linearly independent, it is often\n" +"very helpful to try to find the correct set and function to sum over, then try to satisfy the assumptions\n" +"to prove that the function must be zero. Since the goal is to prove that `f = g`, maybe try to prove\n" +"instead that `f - g = 0`, so you can try proving the assumptions in `hS` with the function `f - g`. You\n" +"also need to pick the correct set to be summing over. Since this set must contain both `s` and `t`, you\n" +"can use `s ∪ t`. Also, note that this will then only prove that `f = g` on the set `s ∪ t`, so you may\n" +"need to use `by_cases` to prove it outside `s ∪ t`.\n" +"\n" +"### Note on hints\n" +"With the use of `have` statements, you may have multiple goals at the same time. While this is not a\n" +"problem when writing the proof, the hint system may get confused. Starting to type where you\n" +"intend to write your next tactic will help clear up what goal you are working on, so it will help the hint\n" +"system. However, in general, try to follow your intuition without blindly following the hints." +msgstr "" + #: Game.Levels.VectorSpaceWorld.Level03 msgid "We now have many theorems relating to vector spaces! In the next levels, we will introduce\n" "the idea of a \"subspace\"." @@ -1258,13 +1269,6 @@ msgid "This is a proof that `0 • w = 0`, or that scaling any vector by `0` giv "scalar multiplication of a vector." msgstr "" -#: Game.Levels.TutorialWorld.Level10 -msgid "'add_succ' is a proof that `n + Nat.succ m = Nat.succ (n + m)`.\n" -"\n" -"The reason for the name is that the theorem proves that adding the successor of a number is equal to\n" -"the successor of addind that number." -msgstr "" - #: Game.Levels.InnerProductWorld.Level02 msgid "Zero Norm if and only if Zero Vector" msgstr "" @@ -1294,25 +1298,6 @@ msgid "## Summary\n" "`rw[(add_dist 2 5 x).symm]` will change the goal to `(2 + 5) * x = y`." msgstr "" -#: Game.Levels.TutorialWorld.Level10 -msgid "The `induction` tactic is a powerful tool to help you to prove statements involving natural numbers.\n" -"It splits a proof into two cases: a base case and an inductive step. The base case is the smallest\n" -"natural number you need to prove the proof for. The inductive step proves the theorem for all other\n" -"numbers. In the inductive step, you can assume the theorem holds for some value `n`, and must then\n" -"prove that it holds for `n + 1`, also written as `Nat.succ n`, the successor of `n`. Induction can\n" -"also be used to prove theorems about objects indexed by natural numbers, such as vectors whose\n" -"dimension can be described by a natural number.\n" -"\n" -"The syntax for the `induction` tactic in Lean 4 is `induction n with | zero => ... | succ n h => ...`.\n" -"As long as `n` is an arbitrary natural number in the proof, this will do induction on `n`, where\n" -"`zero` handles the base case, `succ n` is the successor case, and `h` is the induction hypothesis.\n" -"\n" -"This level also uses a new theorem: `add_succ`. `add_succ` is a proof that\n" -"`n + Nat.succ m = Nat.succ (n + m)`, for any `n, m : ℕ`.\n" -"\n" -"**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." -msgstr "" - #: Game.Levels.LinearIndependenceSpanWorld.Level07 msgid "`sub_smul` is a proof that subtraction distributes over scalar multiplication. `sub_smul a b c` is a proof\n" "that `(a - b) • c = a • c - b • c`." @@ -1344,6 +1329,10 @@ msgid "## Summary\n" "to `x ≥ 0`." msgstr "" +#: Game.Levels.LinearMapsWorld.Level04 +msgid "The null space of any linear map is a subspace of the domain." +msgstr "" + #: Game.Levels.VectorSpaceWorld.Level04 #: Game.Levels.VectorSpaceWorld.Level04 msgid "This is a proof that any subspace contains the zero vector." @@ -1426,6 +1415,10 @@ msgstr "" msgid "Linear maps preserve linear combinations of two vectors." msgstr "" +#: Game.Levels.LinearMapsWorld.Level04 +msgid "The null space of a linear map is a subspace." +msgstr "" + #: Game.Levels.LinearMapsWorld.Level08 msgid "If T is injective, then its null space contains only zero." msgstr "" @@ -1512,19 +1505,6 @@ msgid "## Summary\n" "If you have a hypothesis `h: False`, and a goal `Q`, `exfalso; exact h` will solve the goal`" msgstr "" -#: Game.Levels.TutorialWorld.Level01 -msgid "Most levels in this game will require you to prove a mathematical theorem. In the middle of the\n" -"screen, you will see your \"Active Goal\", which includes \"Objects:\" `x: ℝ` and a \"Goal\" `x=x`.\n" -"In later levels, you may also get a \"Assumptions\" line. Your objects and assumptions are what you\n" -"have to work with. In this case, we know that `x` is in `ℝ`, which means `x` is a real number.\n" -"From this, we have to prove our goal, that `x=x`.\n" -"\n" -"The first tactic we will use is the `rfl` tactic. `rfl` stands for \"reflexivity\". `rfl` will solve\n" -"goals when the left side of an equation is the same as the right side, at least up to definitions.\n" -"\n" -"**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." -msgstr "" - #: Game.Levels.InnerProductWorld.Level03 msgid "## Summary\n" "`ring` acts very similar to `simp` and `linarith` in that it will attempt to solve the goal for you.\n" @@ -1986,10 +1966,6 @@ msgstr "" msgid "If T maps v to w, then w is in the range of T." msgstr "" -#: Game.Levels.LinearMapsWorld.Level04 -msgid "Linear Maps Preserve Zero" -msgstr "" - #: Game.Levels.InnerProductWorld.Level03 msgid "The product of two non-negative real numbers is non-negative." msgstr "" @@ -1998,8 +1974,16 @@ msgstr "" msgid "If T is injective and maps v to w, then v ≠ 0 if and only if w ≠ 0." msgstr "" -#: Game.Levels.LinearMapsWorld.Level04 -msgid "Linear maps preserve zero." +#: Game.Levels.TutorialWorld.Level02 +msgid "The second tactic we will look at is the rewrite tactic. This tactic is how you \"substitute in\"\n" +"a value for something you know is equal. If you have an assumption `h: A=B`, and your goal is to\n" +"prove something about `A`, you can replace `A` with `B`, since they are equal.\n" +"\n" +"In this level, the goal is to prove `2 * y = 2 * (x + 7)`. You also have an assumption `h: y = x + 7`.\n" +"Writing `rw[h]` will rewrite `y` as `x + 7` in the goal.\n" +"\n" +"Also note that the `rw` tactic will automatically attempt the `rfl` tactic after it rewrites, so if\n" +"after the rewrite the goal is of the form `X = X`, it will automatically be solved." msgstr "" #: Game.Levels.VectorSpaceWorld.Level03 @@ -2073,6 +2057,21 @@ msgid "## Summary\n" "Use when dealing with mixed numeric types (ℕ, ℤ, ℚ, ℝ, ℂ) to simplify coercion expressions." msgstr "" +#: Game.Levels.TutorialWorld.Level05 +msgid "## Summary\n" +"\n" +"If we have some object or function with some definition, `unfold object` will rewrite the object\n" +"with its definition in the goal. Lean often unfolds terms automatically, but some tactics and definitions\n" +"are not unfolded automatically. The `unfold` tactic also helps make it easier to take the next steps.\n" +"\n" +"`unfold object at h` unfolds at the assumption `h` whereas `unfold object at *` unfolds everywhere.\n" +"\n" +"## Example:\n" +"\n" +"If you have a goal `(P → Q) → (¬ Q → ¬ P)`, with `¬ P` (\\\"Not\\\" P) being defined as `P → False`,\n" +"using `unfold Not` will change the goal to `(P → Q) → ((Q → False) → (P → False))`" +msgstr "" + #: Game.Levels.LinearIndependenceSpanWorld.Level08 msgid "## Summary\n" "\n" @@ -2253,12 +2252,6 @@ msgid "We won't prove it in this game (although it isn't too difficult), but any "a single vector is also linearly independent." msgstr "" -#: Game.Levels.LinearMapsWorld.Level04 -msgid "You've proven that linear maps always preserve zero!\n" -"\n" -"This simple but fundamental property will be the foundation for many more sophisticated results about linear maps. Every linear map, no matter how complex, must map 0 to 0." -msgstr "" - #: Game.Levels.TutorialWorld.Level07 msgid "The `linarith` tactic aims to simplify the process of proofs. Specifically, it solves certain kinds\n" "of linear equalities and inequalities. It attempts to solve or simplify the goal using the hypotheses\n" @@ -2293,6 +2286,10 @@ msgstr "" msgid "Linear Independence of Subsets" msgstr "" +#: Game.Levels.LinearMapsWorld.Level04 +msgid "You've proven that the null space of any linear map $T : V \\to W$ is a subspace of $V$! Next, we'll show the same for the range of $T$." +msgstr "" + #: Game.Levels.InnerProductWorld msgid "Welcome to the Inner Product World! In this world, we introduce the idea of the inner product,\n" "along with orthogonality and vector norms. You will prove many familiar theorems, such as the Pythagorean\n" @@ -2417,6 +2414,42 @@ msgid "In this level, we will introduce the span of a set of vectors. The span o "**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." msgstr "" +#: Game.Levels.LinearIndependenceSpanWorld.Level01 +msgid "The first level of this world will introduce the definition of a linear combination. Let's\n" +"say we want to express that some vector `x` is a linear combination of some set `S ⊆ V`. This means\n" +"that there is some number of elements in `S`, that after some scalar multiplication, sums to `x`.\n" +"Since infinite sums are difficult (and sometimes impossible) to work with, we can't simply sum over\n" +"all of `S`. Instead, we take some smaller subset `s : Finset V`, with `↑s ⊆ S`, and sum over that.\n" +"Note here the `↑` character. This simply takes our finite set `s`, which is a `Finset`, and treats it\n" +"as a `Set`.\n" +"\n" +"Once we have the set we are summing over `s`, we need to also multiply the elements of `s` by scalars.\n" +"We do this with a function `f : V → K`, where each element of `s` gets mapped to the scalar we multiply by.\n" +"Now, we are able to understand the definition of linear combinations:\n" +"\n" +"```\n" +"def is_linear_combination (S : Set V) (x : V) : Prop :=\n" +"∃ (s : Finset V) (f : V → K),\n" +" (↑s ⊆ S) ∧ (x = Finset.sum s (fun v => f v • v))\n" +"```\n" +"\n" +"### The Goal\n" +"The goal of this level is to prove that if `v ∈ S`, then `v` is a linear combination of `s`. This can\n" +"be done simply by summing over the set `{v}`, with only multiplying by the scalar 1.\n" +"\n" +"### Defining functions\n" +"In this level, we need to use the `use` tactic to specify a function `f`. A very versatile way of doing\n" +"this is with the `fun` keyword. This allows you to write the function, and for Lean to accept it as a function.\n" +"For example, to write `f(x) = x²`, we can say `fun x => x * x`.\n" +"\n" +"### The return of the `simp` tactic\n" +"Since the levels in this world will become more difficult than in the last world, you are again allowed\n" +"to use the `simp` tactic. It is able to solve most simple equalities with vectors, and helps greatly\n" +"when trying to simplify properties of sets.\n" +"\n" +"**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." +msgstr "" + #: Game msgid "# Welcome to the Linear Algebra Game!\n" "\n" @@ -2584,6 +2617,28 @@ msgid "Just as we proved that the null space is always a subspace, we'll now pro "**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." msgstr "" +#: Game.Levels.LinearMapsWorld.Level04 +msgid "We've seen that the null space of a linear map always contains zero. Now we'll prove the stronger result: the null space is always a **subspace** of the domain.\n" +"\n" +"## The Three Subspace Properties\n" +"\n" +"Recall that to show a set $S$ is a subspace, we must verify:\n" +"\n" +"1. **Non-empty**: $S$ contains at least one element (we'll use $0$).\n" +"2. **Closed under addition**: if $u, v \\in S$, then $u + v \\in S$.\n" +"3. **Closed under scalar multiplication**: if $v \\in S$ and $a$ is a scalar, then $a \\cdot v \\in S$.\n" +"\n" +"## Why This Matters\n" +"\n" +"Together with Level 5, this shows every linear map produces two natural subspaces for free: the null space in $V$ and the range in $W$.\n" +"\n" +"### Your Goal\n" +"\n" +"Prove that the null space of any linear map is a subspace.\n" +"\n" +"**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." +msgstr "" + #: Game.Levels.VectorSpaceWorld.Level01 msgid "∀ (a b : K) (x : V), (a * b) • x = a • (b • x)\n" "`mul_smul` is one of the axioms of a vector space. It is a proof that if we know `vs : VectorSpace K V`,\n" @@ -2622,10 +2677,18 @@ msgid "Now we'll explore a crucial property of injective linear maps: they prese "**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." msgstr "" +#: Game.Levels.LinearMapsWorld.Level04 +msgid "The Null Space is a Subspace" +msgstr "" + #: GameServer.RpcHandlers msgid "level completed! 🎉" msgstr "" +#: Game.Levels.LinearMapsWorld.Level04 +msgid "Linear maps preserve zero: $T(0) = 0$." +msgstr "" + #: Game.Levels.TutorialWorld.Level06 msgid "The `cases'` and `exfalso` tactics" msgstr "" @@ -2655,10 +2718,6 @@ msgid "We now introduce orthogonality. Two vectors being orthogonal is equivalen "**Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints." msgstr "" -#: Game.Levels.LinearMapsWorld.Level04 -msgid "Every linear map maps the zero vector to the zero vector." -msgstr "" - #: Game.Levels.LinearIndependenceSpanWorld.Level07 msgid "## Summary\n" "The `by_cases` tactic is able to create a new hypothesis, and split the goal into two cases: one where\n" @@ -2850,69 +2909,6 @@ msgid "## Welcome to Vector Space World!\n" "Ready to begin your journey into vector spaces? Let's start proving theorems!" msgstr "" -#: Game.Levels.LinearIndependenceSpanWorld.Level07 -msgid "This is the \"boss level\" of the Linear Independence and Span World. This level is a\n" -"proof that in a linearly independent set, linear combinations are unique. There are also a few new tactics\n" -"and multiple new theorems you should use.\n" -"\n" -"### The Goal\n" -"In this level, we have 5 objects and 6 hypotheses about those objects. We have the set `S : Set V`,\n" -"which is the linearly independent set we are working with. We also have `s` and `f`, which are the set\n" -"and function we are summing over to get the first linear combination, and `t` and `g` are the second\n" -"linear combination. We have `hs : linear_independent_v K V S`, which states that `S` is linearly independent,\n" -"`hs : ↑s ⊆ S` and `ht : ↑t ⊆ S`, which state that `s` and `t` are both in `S`, so are valid linear\n" -"combinations of `S`. We know `hf0 : ∀ v ∉ s, f v = 0` and a similar `hg0`, which state that both functions\n" -"are zero outside of their domain. This helps us prove `f = g`, since otherwise we wouldn't know what\n" -"the values of `f` and `g` would be outside of `s` and `t`. Lastly, we have `heq : Finset.sum s (fun v => f v • v) = Finset.sum t (fun v => g v • v)`,\n" -"which shows that the two linear combinations are equal. We then must pove that `f = g`\n" -"\n" -"**Note:** This level may experience a hint display issue where hints repeat. If you see the same hint multiple times, the level is still working correctly - just continue with your proof as normal.\n" -"\n" -"### The `specialize` tactic\n" -"The `specialize` tactic can be thought of as the opposite of `use`. While `use` helps specify a value\n" -"for a `∃` in the goal, `specialize` specifies a value for a `∀` in a hypothesis. For example, if you\n" -"have a hypothesis `h : ∀ v : V, v • 1 = v`, and you have a vector `x : V`, then `specialize h x` will\n" -"change `h` to `h : x • 1 = x`. `specialize` also works if `h` is an implication. If `h1 : P → Q` is a\n" -"hypothesis, and `h2 : P` is a proof of `P`, then `specialize h1 h2` will change `h2` to `h2 : Q`.\n" -"\n" -"### The `by_cases` tactic\n" -"The `by_cases` tactic helps you prove something by cases. If you want to prove a statement about vectors\n" -"in `V`, but you want to split into cases where `v = 0` or `v ≠ 0`, `by_cases hv : v = 0` will split the\n" -"goal into two subgoals: one where you have a hypothesis `hv : v = 0`, and another where you have a hpyothesis\n" -"`hv : v ≠ 0`.\n" -"\n" -"### The `funext` tactic\n" -"The `funext` tactic lets you prove statements about functions. It works similarly to the `intro` tactic,\n" -"where you introduce an arbitrary object, but instead of introducing from a `∀` statement, it works if\n" -"you have a goal of the form `f = g`, where `funext x` will change the goal to the form `f x = g x`, and\n" -"give you an arbitrary `x` in the domain of `f` and `g`.\n" -"\n" -"### New theorems\n" -"This level requires multiple new theorems, particularly ones about Finsets and sums. There are two theorems\n" -"about vector spaces that can be proven quite easily, but they are still nice to have without needing\n" -"to prove them first. Instead of explaining them all here, you can look at them on the right side of\n" -"the screen. The new theorems are: `coe_union`, `union_subset`, `sub_smul`, 'sum_add_distrib', 'sum_sub_distrib',\n" -"`subset_union_left`, `subset_union_right`, `sum_subset`, `sub_eq_zero`, and `notMem_union`.\n" -"If you need more theorems, you can either prove them in lemmas, or if you want, you can go to the world\n" -"select menu and turn \"Rules\" to \"none\", which should allow you to use any tactic or theorem in Lean.\n" -"\n" -"### Proof overview\n" -"If you look at the hypotheses you have, the most important ones are that S is linearly independent and\n" -"that the two sums are equal. When you have a statement that a set is linearly independent, it is often\n" -"very helpful to try to find the correct set and function to sum over, then try to satisfy the assumptions\n" -"to prove that the function must be zero. Since the goal is to prove that `f = g`, maybe try to prove\n" -"instead that `f - g = 0`, so you can try proving the assumptions in `hS` with the function `f - g`. You\n" -"also need to pick the correct set to be summing over. Since this set must contain both `s` and `t`, you\n" -"can use `s ∪ t`. Also, note that this will then only prove that `f = g` on the set `s ∪ t`, so you may\n" -"need to use `by_cases` to prove it outside `s ∪ t`.\n" -"\n" -"### Note on hints\n" -"With the use of `have` statements, you may have multiple goals at the same time. While this is not a\n" -"problem when writing the proof, the hint system may get confused. Starting to type where you\n" -"intend to write your next tactic will help clear up what goal you are working on, so it will help the hint\n" -"system. However, in general, try to follow your intuition without blindly following the hints." -msgstr "" - #: Game.Levels.TutorialWorld.Level03 msgid "In this level, we will introduce two tactics: `intro`, and `exact`\n" "Our goal is to prove that for any proposition (a True/False statement) `P`, we know that `P → P`.\n" diff --git a/Game/Levels/LinearMapsWorld/Level04.lean b/Game/Levels/LinearMapsWorld/Level04.lean index 4e1474e..d736575 100644 --- a/Game/Levels/LinearMapsWorld/Level04.lean +++ b/Game/Levels/LinearMapsWorld/Level04.lean @@ -1,57 +1,101 @@ import Game.Levels.LinearMapsWorld.Level03 +import Game.Levels.VectorSpaceWorld namespace LinearAlgebraGame World "LinearMapsWorld" Level 4 -Title "Linear Maps Preserve Zero" +Title "The Null Space is a Subspace" Introduction " -Now let's prove a fundamental property that every linear map must satisfy: they always map the zero vector to the zero vector. +We've seen that the null space of a linear map always contains zero. Now we'll prove the stronger result: the null space is always a **subspace** of the domain. -## The Key Insight +## The Three Subspace Properties -This might seem obvious, but it's an important consequence of linearity that we'll use in many future proofs. +Recall that to show a set $S$ is a subspace, we must verify: + +1. **Non-empty**: $S$ contains at least one element (we'll use $0$). +2. **Closed under addition**: if $u, v \\in S$, then $u + v \\in S$. +3. **Closed under scalar multiplication**: if $v \\in S$ and $a$ is a scalar, then $a \\cdot v \\in S$. ## Why This Matters -The fact that linear maps preserve zero is often the first step in proving that the null space is non-empty, and it's crucial for understanding the structure of linear maps. +Together with Level 5, this shows every linear map produces two natural subspaces for free: the null space in $V$ and the range in $W$. ### Your Goal -Prove that for any linear map T, we have T(0) = 0. + +Prove that the null space of any linear map is a subspace. **Note:** If you see hints appearing multiple times, this is a known issue with the game framework. Simply continue with your proof - the level will work correctly despite any duplicate hints. " open VectorSpace -variable (K V W : Type) [Field K] [AddCommGroup V] [AddCommGroup W] +variable (K V W : Type) [Field K] [AddCommGroup V] [AddCommGroup W] variable [VectorSpace K V] [VectorSpace K W] /-- -Linear maps preserve zero. +Linear maps preserve zero: $T(0) = 0$. -/ TheoremDoc LinearAlgebraGame.linear_map_preserves_zero as "linear_map_preserves_zero" in "Linear Maps" +theorem linear_map_preserves_zero (T : V → W) (hT : is_linear_map_v K V W T) : + T 0 = 0 := + zero_in_null_space K V W T hT + /-- -Every linear map maps the zero vector to the zero vector. +The null space of a linear map is a subspace. -/ -Statement linear_map_preserves_zero (T : V → W) (hT : is_linear_map_v K V W T) : - T 0 = 0 := by - Hint "Use the homogeneity property with scalar 0. Apply hT.2 with scalar 0 and vector 0." - Hint (hidden := true) "Try `have h : T ((0 : K) • (0 : V)) = (0 : K) • T 0 := hT.2 (0 : K) 0`" - have h : T ((0 : K) • (0 : V)) = (0 : K) • T 0 := hT.2 (0 : K) 0 - Hint "Simplify: 0 • v = 0 for any vector v. Use simp to clean up the zeros." - Hint (hidden := true) "Try `simp at h`" - simp at h - Hint "Now h gives us exactly what we need: T 0 = 0." - Hint (hidden := true) "Try `exact h`" - exact h +TheoremDoc LinearAlgebraGame.null_space_is_subspace as "null_space_is_subspace" in "Linear Maps" -Conclusion " -You've proven that linear maps always preserve zero! +NewTheorem LinearAlgebraGame.linear_map_preserves_zero -This simple but fundamental property will be the foundation for many more sophisticated results about linear maps. Every linear map, no matter how complex, must map 0 to 0. +/-- +The null space of any linear map is a subspace of the domain. +-/ +Statement null_space_is_subspace (T : V → W) (hT : is_linear_map_v K V W T) : + isSubspace (K := K) (V := V) (null_space_v K V W T) := by + Hint "We need to verify the three subspace properties." + Hint (hidden := true) "Try `constructor`" + constructor + Hint "First, show the null space is non-empty by exhibiting 0 as a member." + · -- Non-empty + Hint (hidden := true) "Try `use 0`" + use 0 + Hint "Now show 0 is in the null space — this is exactly `zero_in_null_space`." + Hint (hidden := true) "Try `exact zero_in_null_space K V W T hT`" + exact zero_in_null_space K V W T hT + Hint (hidden := true) "Try `constructor`" + constructor + Hint "For closure under addition: assume T(x) = 0 and T(y) = 0; show T(x + y) = 0." + · -- Closed under addition + Hint (hidden := true) "Try `intro x y hx hy`" + intro x y hx hy + Hint "Goal `x + y ∈ null_space_v T` unfolds to `T (x + y) = 0`." + Hint (hidden := true) "Try `show T (x + y) = 0`" + show T (x + y) = 0 + Hint "Use additivity (`hT.1`) to split `T (x + y)`, then rewrite using the hypotheses." + Hint (hidden := true) "Try `rw [hT.1 x y, hx, hy]`" + rw [hT.1 x y, hx, hy] + Hint "Finally, simplify `0 + 0`." + Hint (hidden := true) "Try `simp`" + simp + Hint "For closure under scalar multiplication: assume T(x) = 0; show T(a • x) = 0." + · -- Closed under scalar multiplication + Hint (hidden := true) "Try `intro a x hx`" + intro a x hx + Hint "Goal `a • x ∈ null_space_v T` unfolds to `T (a • x) = 0`." + Hint (hidden := true) "Try `show T (a • x) = 0`" + show T (a • x) = 0 + Hint "Use homogeneity (`hT.2`) to pull the scalar out, then rewrite using the hypothesis." + Hint (hidden := true) "Try `rw [hT.2 a x, hx]`" + rw [hT.2 a x, hx] + Hint "Finally, simplify `a • 0`." + Hint (hidden := true) "Try `simp`" + simp + +Conclusion " +You've proven that the null space of any linear map $T : V \\to W$ is a subspace of $V$! Next, we'll show the same for the range of $T$. " end LinearAlgebraGame diff --git a/Game/Levels/LinearMapsWorld/Level05.lean b/Game/Levels/LinearMapsWorld/Level05.lean index a1cb85e..73b6e2a 100644 --- a/Game/Levels/LinearMapsWorld/Level05.lean +++ b/Game/Levels/LinearMapsWorld/Level05.lean @@ -41,8 +41,6 @@ The range of a linear map is a subspace. -/ TheoremDoc LinearAlgebraGame.range_is_subspace as "range_is_subspace" in "Linear Maps" -NewTheorem LinearAlgebraGame.linear_map_preserves_zero - /-- The range of any linear map is a subspace of the codomain. -/