From 19e02514a962077ceea83ae4a1c47e86bb45dc7f Mon Sep 17 00:00:00 2001 From: Aleph <14uburu@protonmail.com> Date: Fri, 7 Nov 2025 17:59:08 +0100 Subject: [PATCH] Add new theorems and proofs Automated commit at 20251107_165907 --- MathTest.lean | 1 + MathTest/Theorems/RationalSequenceExists.lean | 11 + ttt | 1647 +++++++++++++++++ 3 files changed, 1659 insertions(+) create mode 100644 MathTest/Theorems/RationalSequenceExists.lean create mode 100644 ttt diff --git a/MathTest.lean b/MathTest.lean index 5be7cdf..6b1d913 100644 --- a/MathTest.lean +++ b/MathTest.lean @@ -1 +1,2 @@ import MathTest.Basic +import MathTest.Theorems.RationalSequenceExists diff --git a/MathTest/Theorems/RationalSequenceExists.lean b/MathTest/Theorems/RationalSequenceExists.lean new file mode 100644 index 0000000..ecf9136 --- /dev/null +++ b/MathTest/Theorems/RationalSequenceExists.lean @@ -0,0 +1,11 @@ +import Mathlib + +theorem rational_sequence_exists : + ∃ s : Nat → Rat, ∀ a d : Rat, ∃ t : Nat, s t = a + d * t := by + classical + obtain ⟨f, hf⟩ := exists_surjective_nat (α := Rat × Rat) + refine ⟨fun n => (f n).1 + (f n).2 * n, ?_⟩ + intro a d + obtain ⟨t, ht⟩ := hf ⟨a, d⟩ + refine ⟨t, ?_⟩ + simpa [ht] diff --git a/ttt b/ttt new file mode 100644 index 0000000..8e4ef39 --- /dev/null +++ b/ttt @@ -0,0 +1,1647 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + GitHub - winger/math-test + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + + +
+ Skip to content + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + + + +
+ +
+ + + + + + + + +
+ + + + + +
+ + + + + + + + + +
+
+
+ + + + + + + + + + + + + + + +
+ +
+ +
+ +
+ + + + / + + math-test + + + Public +
+ + +
+ +
+ + +
+
+ +
+
+ + + +
+ + + 0 + stars + + + 0 + forks + + + Branches + + + Tags + + + Activity +
+
+
+
+ + Star + +
+
+
+ Notifications + You must be signed in to change notification settings + +
+ + + + +
+
+ +
+ + + + +
+ + + + + + +
+ + + + + + +

winger/math-test

+
+
+ +
+
+ + + + + +
BranchesTags

Repository files navigation

math-test

+

GitHub configuration

+

To set up your new GitHub repository, follow these steps:

+
    +
  • Under your repository name, click Settings.
    • +
  • In the Actions section of the sidebar, click "General".
    • +
  • Check the box Allow GitHub Actions to create and approve pull requests.
    • +
  • Click the Pages section of the settings sidebar.
    • +
  • In the Source dropdown menu, select "GitHub Actions".
    • +
+

After following the steps above, you can remove this section from the README file.

+
+ + + + +
+
+ +
+
+
+
+

About

+ +
+ No description, website, or topics provided. +
+ + +

Resources

+
+ + + Readme +
+ + + + + + + + + + + + +
+ + Activity
+ + +

Stars

+
+ + 0 + stars
+ +

Watchers

+
+ + 0 + watching
+ +

Forks

+
+ + 0 + forks
+ + +
+ + Report repository +
+
+ +
+
+ + +
+
+

+ Releases

+ +
No releases published
+ +
+
+ + + +
+
+ +

+ Packages +

+ + +
+ No packages published
+
+ + + +
+
+ + + + + +
+
+

Languages

+
+ + +
+ + +
+
+ +
+
+ +
+ +
+ + +
+ + + + +
+
+ +
+ + + + + + + + + + + + + + + + + + + + + + +
+
+
+ + +