Skip to content

Commit

Permalink
chore: make Antisymm a Prop (#4666)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Jul 7, 2024
1 parent 4ed7947 commit 64eeba7
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1867,7 +1867,7 @@ instance : Subsingleton (Squash α) where
/--
`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
-/
class Antisymm {α : Sort u} (r : α → α → Prop) where
class Antisymm {α : Sort u} (r : α → α → Prop) : Prop where
/-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
antisymm {a b : α} : r a b → r b a → a = b

Expand Down

0 comments on commit 64eeba7

Please sign in to comment.