Skip to content

Commit

Permalink
chore(Init/Order/Defs): alias for le_antisymm (#12545)
Browse files Browse the repository at this point in the history
  • Loading branch information
madvorak committed Apr 30, 2024
1 parent d29b378 commit 9de65eb
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions Mathlib/Init/Order/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,8 @@ theorem le_antisymm : ∀ {a b : α}, a ≤ b → b ≤ a → a = b :=
PartialOrder.le_antisymm _ _
#align le_antisymm le_antisymm

alias eq_of_le_of_le := le_antisymm

theorem le_antisymm_iff {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a :=
fun e => ⟨le_of_eq e, le_of_eq e.symm⟩, fun ⟨h1, h2⟩ => le_antisymm h1 h2⟩
#align le_antisymm_iff le_antisymm_iff
Expand Down

0 comments on commit 9de65eb

Please sign in to comment.