Skip to content

Commit

Permalink
Update lean4/src/putnam_1996_a4.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
GeorgeTsoukalas authored Oct 28, 2024
1 parent 1ce0f88 commit f74fe66
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lean4/src/putnam_1996_a4.lean
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ theorem putnam_1996_a4
(S : Set (A × A × A))
(hSdistinct : ∀ a b c : A, ⟨a, b, c⟩ ∈ S → a ≠ b ∧ b ≠ c ∧ a ≠ c)
(hS1 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨b, c, a⟩ ∈ S)
(hS2 : ∀ a b c : A, a ≠ c → ⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S)
(hS2 : ∀ a b c : A, a ≠ c → (⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S))
(hS3 : ∀ a b c d : A, (⟨a, b, c⟩ ∈ S ∧ ⟨c, d, a⟩ ∈ S) ↔ (⟨b,c,d⟩ ∈ S ∧ ⟨d,a,b⟩ ∈ S))
: ∃ g : A → ℝ, Injective g ∧ (∀ a b c : A, g a < g b ∧ g b < g c → ⟨a,b,c⟩ ∈ S) :=
sorry

0 comments on commit f74fe66

Please sign in to comment.