From 4fde5a554745253ba37fb31dbd63eda984eadc58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 16 Oct 2024 10:27:02 +0000 Subject: [PATCH] feat(SetTheory/Ordinal/Exponential): more lemmas on `opow` (#17804) --- Mathlib/SetTheory/Ordinal/Exponential.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean index 902f6a296c035..3fad6ff39bde5 100644 --- a/Mathlib/SetTheory/Ordinal/Exponential.lean +++ b/Mathlib/SetTheory/Ordinal/Exponential.lean @@ -157,6 +157,9 @@ theorem opow_le_opow_left {a b : Ordinal} (c : Ordinal) (ab : a ≤ b) : a ^ c (opow_le_of_limit a0 l).2 fun b' h => (IH _ h).trans (opow_le_opow_right ((Ordinal.pos_iff_ne_zero.2 a0).trans_le ab) h.le) +theorem opow_le_opow {a b c d : Ordinal} (hac : a ≤ c) (hbd : b ≤ d) (hc : 0 < c) : a ^ b ≤ c ^ d := + (opow_le_opow_left b hac).trans (opow_le_opow_right hc hbd) + theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b := by nth_rw 1 [← opow_one a] cases' le_or_gt a 1 with a1 a1 @@ -167,8 +170,12 @@ theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b := b rw [a1, one_opow, one_opow] rwa [opow_le_opow_iff_right a1, one_le_iff_pos] +theorem left_lt_opow {a b : Ordinal} (ha : 1 < a) (hb : 1 < b) : a < a ^ b := by + conv_lhs => rw [← opow_one a] + rwa [opow_lt_opow_iff_right ha] + theorem right_le_opow {a : Ordinal} (b : Ordinal) (a1 : 1 < a) : b ≤ a ^ b := - (isNormal_opow a1).id_le _ + (isNormal_opow a1).le_apply theorem opow_lt_opow_left_of_succ {a b c : Ordinal} (ab : a < b) : a ^ succ c < b ^ succ c := by rw [opow_succ, opow_succ]