Update Thu Sep 12 23:49:20 EDT 2024

Author: hrmacbeth

Math2001/Homework/hw2.lean

@@ -0,0 +1,34 @@
+/- Copyright (c) Heather Macbeth, 2024.  All rights reserved. -/
+import Mathlib.Data.Real.Basic
+import Library.Basic
+import AutograderLib
+
+math2001_init
+
+/-! # Homework 2
+
+Don't forget to compare with the text version,
+https://github.com/hrmacbeth/math2001/wiki/Homework-2,
+for clearer statements and any special instructions. -/
+
+
+@[autograded 5]
+theorem problem1 {x : ℚ} (h1 : x ^ 2 = 9) (h2 : 1 < x) : x = 3 := by
+  sorry
+
+@[autograded 5]
+theorem problem2 {s : ℚ} (h1 : 3 * s ≤ -15) (h2 : 2 * s ≥ -10) : s = -5 := by
+  sorry
+
+@[autograded 4]
+theorem problem3 {t : ℚ} (h : t = 2 ∨ t = -3) : t ^ 2 + t - 6 = 0 := by
+  sorry
+
+@[autograded 5]
+theorem problem4 {x : ℤ} : 3 * x ≠ 10 := by
+  sorry
+
+@[autograded 6]
+theorem problem5 {x y : ℝ} (h1 : 2 ≤ x ∨ 2 ≤ y) (h2 : x ^ 2 + y ^ 2 = 4) :
+    x ^ 2 * y ^ 2 = 0 := by
+  sorry