From 4bfe8e8a7271fb01a68f84376728818fa9bf0a50 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 11 Jun 2021 13:26:14 +0000 Subject: [PATCH] feat(algebra/order_functions): lt_max_of_lt_ (#7849) --- src/algebra/order_functions.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/algebra/order_functions.lean b/src/algebra/order_functions.lean index 3fdb37aa29d47..41500ea59eabe 100644 --- a/src/algebra/order_functions.lean +++ b/src/algebra/order_functions.lean @@ -31,8 +31,12 @@ lemma max_le_max : a ≤ c → b ≤ d → max a b ≤ max c d := sup_le_sup lemma min_le_min : a ≤ c → b ≤ d → min a b ≤ min c d := inf_le_inf lemma le_max_left_of_le : a ≤ b → a ≤ max b c := le_sup_left_of_le lemma le_max_right_of_le : a ≤ c → a ≤ max b c := le_sup_right_of_le +lemma lt_max_of_lt_left (h : a < b) : a < max b c := h.trans_le (le_max_left b c) +lemma lt_max_of_lt_right (h : a < c) : a < max b c := h.trans_le (le_max_right b c) lemma min_le_left_of_le : a ≤ c → min a b ≤ c := inf_le_left_of_le lemma min_le_right_of_le : b ≤ c → min a b ≤ c := inf_le_right_of_le +lemma min_lt_of_left_lt (h : a < c) : min a b < c := (min_le_left a b).trans_lt h +lemma min_lt_of_right_lt (h : b < c) : min a b < c := (min_le_right a b).trans_lt h lemma max_min_distrib_left : max a (min b c) = min (max a b) (max a c) := sup_inf_left lemma max_min_distrib_right : max (min a b) c = min (max a c) (max b c) := sup_inf_right lemma min_max_distrib_left : min a (max b c) = max (min a b) (min a c) := inf_sup_left