Included Real scope for notational purposes.

trishullab · Aug 27, 2024 · 3052cbb · 3052cbb
1 parent 7125999
commit 3052cbb
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/lean4/src/putnam_1980_b1.lean b/lean4/src/putnam_1980_b1.lean
@@ -1,9 +1,11 @@
 import Mathlib
 open BigOperators
 
+open Real
+
 abbrev putnam_1980_b1_solution : Set ℝ := sorry
 -- {c : ℝ | c ≥ 1 / 2}
 theorem putnam_1980_b1
 (c : ℝ)
-: (∀ x : ℝ, (Real.exp x + Real.exp (-x)) / 2 ≤ Real.exp (c * x ^ 2)) ↔ c ∈ putnam_1980_b1_solution :=
+: (∀ x : ℝ, (exp x + exp (-x)) / 2 ≤ exp (c * x ^ 2)) ↔ c ∈ putnam_1980_b1_solution :=
 sorry