From f5c2d95550507e1ccdced459c773900a9b7e4af8 Mon Sep 17 00:00:00 2001 From: ZRTMRH Date: Sat, 18 Apr 2026 15:38:50 -0400 Subject: [PATCH] fix: consolidate redundant theorem tabs (closes #13) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Move TheoremDoc for Set.union_subset from LinearIndependenceSpanWorld/Level07 to VectorSpaceWorld/Level05, alongside its NewTheorem. Previously the theorem fell into a namespace-default "Set" tab (with only itself) when first introduced, before its TheoremDoc was seen. Now it lands in "Sets" immediately. - In InnerProductWorld/Level03, unify tab names to the Unicode form used elsewhere in the world: "Real Numbers" → "ℝ" (3x), "Complex Numbers" → "ℂ" (2x). Eliminates side-by-side duplicate tabs for the same concept. Co-Authored-By: Claude Opus 4.7 --- Game/Levels/InnerProductWorld/Level03.lean | 10 +++++----- Game/Levels/LinearIndependenceSpanWorld/Level07.lean | 6 ------ Game/Levels/VectorSpaceWorld/Level05.lean | 6 ++++++ 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Game/Levels/InnerProductWorld/Level03.lean b/Game/Levels/InnerProductWorld/Level03.lean index add14fc..ff3a3d6 100644 --- a/Game/Levels/InnerProductWorld/Level03.lean +++ b/Game/Levels/InnerProductWorld/Level03.lean @@ -98,17 +98,17 @@ NewTactic ring /-- The real part of a sum of complex numbers equals the sum of their real parts. -/ -TheoremDoc Complex.add_re as "Complex.add_re" in "Complex Numbers" +TheoremDoc Complex.add_re as "Complex.add_re" in "ℂ" /-- The real part of a complex conjugate equals the real part of the original number. -/ -TheoremDoc Complex.conj_re as "Complex.conj_re" in "Complex Numbers" +TheoremDoc Complex.conj_re as "Complex.conj_re" in "ℂ" /-- The sum of two non-negative real numbers is non-negative. -/ -TheoremDoc add_nonneg as "add_nonneg" in "Real Numbers" +TheoremDoc add_nonneg as "add_nonneg" in "ℝ" /-- Transitivity of the less-than-or-equal relation. @@ -118,7 +118,7 @@ TheoremDoc le_trans as "le_trans" in "Inequalities" /-- The product of two non-negative real numbers is non-negative. -/ -TheoremDoc mul_nonneg as "mul_nonneg" in "Real Numbers" +TheoremDoc mul_nonneg as "mul_nonneg" in "ℝ" /-- The square of a sum: (a + b)² = a² + 2ab + b². @@ -128,7 +128,7 @@ TheoremDoc add_sq as "add_sq" in "Algebra" /-- The square root of a positive real number is positive. -/ -TheoremDoc Real.sqrt_pos as "Real.sqrt_pos" in "Real Numbers" +TheoremDoc Real.sqrt_pos as "Real.sqrt_pos" in "ℝ" NewTheorem norm_nonneg Left.mul_nonneg sq_eq_sq sq_eq_sq₀ mul_assoc Complex.mul_conj Complex.normSq_eq_norm_sq Complex.re_ofReal_mul Complex.add_re Complex.conj_re add_nonneg le_trans mul_nonneg add_sq Real.sqrt_pos LinearAlgebraGame.norm_nonneg_v LinearAlgebraGame.norm_sq_eq diff --git a/Game/Levels/LinearIndependenceSpanWorld/Level07.lean b/Game/Levels/LinearIndependenceSpanWorld/Level07.lean index 7ab78b7..8a44ccd 100644 --- a/Game/Levels/LinearIndependenceSpanWorld/Level07.lean +++ b/Game/Levels/LinearIndependenceSpanWorld/Level07.lean @@ -117,12 +117,6 @@ theorem shows that type casting passes through unions. -/ TheoremDoc Finset.coe_union as "coe_union" in "Sets" -/-- -`union_subset` is a proof that if `a ⊆ c` and `b ⊆ c`, then `a ∪ b ⊆ c`. This means that if you -have two sets that are subsets of the same set, their union is also a subset of that set. --/ -TheoremDoc Set.union_subset as "union_subset" in "Sets" - /-- `sum_add_distrib` is a proof that you can distribute addition over sums. This means that if you have functions `f : A → B`, and `g : A → B`, and some set `s : Finset A`, then diff --git a/Game/Levels/VectorSpaceWorld/Level05.lean b/Game/Levels/VectorSpaceWorld/Level05.lean index 2f71998..efd3272 100644 --- a/Game/Levels/VectorSpaceWorld/Level05.lean +++ b/Game/Levels/VectorSpaceWorld/Level05.lean @@ -54,6 +54,12 @@ Statement subspace_neg {W : Set V} (hW : isSubspace (K := K) (V := V) W) : ∀ ( exact hx -- Add set theory theorems needed by LinearIndependenceSpanWorld +/-- +`union_subset` is a proof that if `a ⊆ c` and `b ⊆ c`, then `a ∪ b ⊆ c`. This means that if you +have two sets that are subsets of the same set, their union is also a subset of that set. +-/ +TheoremDoc Set.union_subset as "union_subset" in "Sets" + NewTheorem Set.union_subset Finset.subset_union_left Finset.subset_union_right Conclusion "You have now completed Vector Space World! The theorems proven here will be very helpful