From 7c44b6f1374ee6584176aada4d67c7c7761fcc9c Mon Sep 17 00:00:00 2001
From: Aleph <14uburu@protonmail.com>
Date: Fri, 7 Nov 2025 18:22:01 +0100
Subject: [PATCH] Add new theorems and proofs

Automated commit at 20251107_172200
---
 MathTest.lean                                  |  1 +
 MathTest/Theorems.lean                         |  2 ++
 ...sequence_intersects_all_rational_lines.lean | 18 ++++++++++++++++++
 3 files changed, 21 insertions(+)
 create mode 100644 MathTest/Theorems.lean
 create mode 100644 MathTest/Theorems/exists_sequence_intersects_all_rational_lines.lean

diff --git a/MathTest.lean b/MathTest.lean
index 5be7cdf..c221361 100644
--- a/MathTest.lean
+++ b/MathTest.lean
@@ -1 +1,2 @@
 import MathTest.Basic
+import MathTest.Theorems
diff --git a/MathTest/Theorems.lean b/MathTest/Theorems.lean
new file mode 100644
index 0000000..c8fc2e5
--- /dev/null
+++ b/MathTest/Theorems.lean
@@ -0,0 +1,2 @@
+import MathTest.Theorems.exists_sequence_intersects_all_rational_lines
+
diff --git a/MathTest/Theorems/exists_sequence_intersects_all_rational_lines.lean b/MathTest/Theorems/exists_sequence_intersects_all_rational_lines.lean
new file mode 100644
index 0000000..4bd3ee6
--- /dev/null
+++ b/MathTest/Theorems/exists_sequence_intersects_all_rational_lines.lean
@@ -0,0 +1,18 @@
+import Mathlib
+
+namespace MathTest
+
+theorem exists_sequence_intersects_all_rational_lines :
+    ∃ s : ℕ → ℚ, ∀ a d : ℚ, ∃ t : ℕ, s t = a + d * (t : ℚ) := by
+  classical
+  let s : ℕ → ℚ := fun t =>
+    match Encodable.decode (α := ℚ × ℚ) t with
+    | some p => p.1 + p.2 * (t : ℚ)
+    | none => 0
+  refine ⟨s, ?_⟩
+  intro a d
+  refine ⟨Encodable.encode (a, d), ?_⟩
+  simp [s, Encodable.encodek (α := ℚ × ℚ) (a, d)]
+
+end MathTest
+