From 3a0dddcce6d2cf948c3eb83cdba4ffd22b8dd85e Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Fri, 3 Sep 2021 20:53:49 +0000 Subject: [PATCH] feat(algebra/order_functions): (min|max)_eq_iff (#8911) Co-authored-by: Yakov Pechersky --- src/algebra/order_functions.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/algebra/order_functions.lean b/src/algebra/order_functions.lean index 800ca13728db8..0d851a82e276f 100644 --- a/src/algebra/order_functions.lean +++ b/src/algebra/order_functions.lean @@ -48,6 +48,19 @@ lemma min_le_max : min a b ≤ max a b := le_trans (min_le_left a b) (le_max_lef @[simp] lemma max_eq_left_iff : max a b = a ↔ b ≤ a := sup_eq_left @[simp] lemma max_eq_right_iff : max a b = b ↔ a ≤ b := sup_eq_right +lemma min_eq_iff : min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a := +begin + split, + { intro h, + refine or.imp (λ h', _) (λ h', _) (le_total a b); + exact ⟨by simpa [h'] using h, h'⟩ }, + { rintro (⟨rfl, h⟩|⟨rfl, h⟩); + simp [h] } +end + +lemma max_eq_iff : max a b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b := +@min_eq_iff (order_dual α) _ a b c + /-- An instance asserting that `max a a = a` -/ instance max_idem : is_idempotent α max := by apply_instance -- short-circuit type class inference