Caught some stragglers.

trishullab · Aug 3, 2024 · 3658d1d · 3658d1d
1 parent 6ab737c
commit 3658d1d
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 3 deletions.
diff --git a/lean4/src/putnam_1971_b2.lean b/lean4/src/putnam_1971_b2.lean
@@ -8,6 +8,7 @@ abbrev putnam_1971_b2_solution : Set (ℝ → ℝ) := sorry
 theorem putnam_1971_b2
 (S : Set ℝ)
 (hS : S = univ \ {0, 1})
-(P : (ℝ → ℝ) → Prop := fun (F : ℝ → ℝ) => ∀ x ∈ S, F x + F ((x - 1)/x) = 1 + x)
+(P : (ℝ → ℝ) → Prop)
+(hP : P = fun (F : ℝ → ℝ) => ∀ x ∈ S, F x + F ((x - 1)/x) = 1 + x)
 : (∀ F ∈ putnam_1971_b2_solution, P F) ∧ ∀ f : ℝ → ℝ, P f → ∃ F ∈ putnam_1971_b2_solution, (∀ x ∈ S, f x = F x) :=
 sorry
diff --git a/lean4/src/putnam_1974_b6.lean b/lean4/src/putnam_1974_b6.lean
@@ -6,7 +6,8 @@ open Set Nat Polynomial Filter Topology
 abbrev putnam_1974_b6_solution : (ℕ × ℕ × ℕ) := sorry
 -- ((2^1000 - 1)/3, (2^1000 - 1)/3, 1 + (2^1000 - 1)/3)
 theorem putnam_1974_b6
-(n : ℤ := 1000)
+(n : ℤ)
+(hn : n = 1000)
 (count0 count1 count2 : ℕ)
 (hcount0 : count0 = {S | S ⊆ Finset.Icc 1 n ∧ S.card ≡ 0 [MOD 3]}.ncard)
 (hcount1 : count1 = {S | S ⊆ Finset.Icc 1 n ∧ S.card ≡ 1 [MOD 3]}.ncard)

diff --git a/lean4/src/putnam_1980_b5.lean b/lean4/src/putnam_1980_b5.lean
@@ -6,7 +6,8 @@ open Set
 abbrev putnam_1980_b5_solution : ℝ → Prop := sorry
 -- fun t : ℝ => 1 ≥ t
 theorem putnam_1980_b5
-(T : Set ℝ := Icc 0 1)
+(T : Set ℝ)
+(hT : T = Icc 0 1)
 (P : ℝ → (ℝ → ℝ) → Prop)
 (Convex : (ℝ → ℝ) → Prop)
 (S : ℝ → Set (ℝ → ℝ))