From 31991729041c1085278d0f45ef413af02541bccb Mon Sep 17 00:00:00 2001 From: YnirPaz Date: Sat, 14 Sep 2024 18:38:41 +0000 Subject: [PATCH] feat(Order/Interval/Set/Monotone): strictMono_of_lt_succ (#16732) Prove `strictMono_of_lt_succ` and `strictAnti_of_pred_lt` for archimedean orders. --- Mathlib/Order/Interval/Set/Monotone.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Order/Interval/Set/Monotone.lean b/Mathlib/Order/Interval/Set/Monotone.lean index 6a9f2ab8f8da3..6b882a9fe70f2 100644 --- a/Mathlib/Order/Interval/Set/Monotone.lean +++ b/Mathlib/Order/Interval/Set/Monotone.lean @@ -188,10 +188,18 @@ theorem strictMonoOn_Iic_of_lt_succ [SuccOrder α] [IsSuccArchimedean α] {n : refine hψ _ (lt_of_lt_of_le ?_ hy) rwa [Function.iterate_succ', Function.comp_apply, lt_succ_iff_not_isMax] +theorem strictMono_of_lt_succ [SuccOrder α] [IsSuccArchimedean α] + (hψ : ∀ m, ψ m < ψ (succ m)) : StrictMono ψ := fun _ _ h ↦ + (strictMonoOn_Iic_of_lt_succ fun m _ ↦ hψ m) h.le le_rfl h + theorem strictAntiOn_Iic_of_succ_lt [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : ∀ m, m < n → ψ (succ m) < ψ m) : StrictAntiOn ψ (Set.Iic n) := fun i hi j hj hij => @strictMonoOn_Iic_of_lt_succ α βᵒᵈ _ _ ψ _ _ n hψ i hi j hj hij +theorem strictAnti_of_pred_lt [SuccOrder α] [IsSuccArchimedean α] + (hψ : ∀ m, ψ (succ m) < ψ m) : StrictAnti ψ := fun _ _ h ↦ + (strictAntiOn_Iic_of_succ_lt fun m _ ↦ hψ m) h.le le_rfl h + theorem strictMonoOn_Ici_of_pred_lt [PredOrder α] [IsPredArchimedean α] {n : α} (hψ : ∀ m, n < m → ψ (pred m) < ψ m) : StrictMonoOn ψ (Set.Ici n) := fun i hi j hj hij => @strictMonoOn_Iic_of_lt_succ αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij