From c02f4f8de096172dc2c6627d34e050108c594752 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Mon, 31 Jul 2023 21:41:48 +0000 Subject: [PATCH] feat(Order/Monotone/Basic): Add Monotone.dual_iff and Antitone.dual_iff (#6157) Add if and only if versions of `Monotone.dual` and `Antitone.dual`. Needed for #5672 Co-authored-by: Christopher Hoskin Co-authored-by: Christopher Hoskin --- Mathlib/Order/Monotone/Basic.lean | 72 ++++++++++++++++++------------- 1 file changed, 42 insertions(+), 30 deletions(-) diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean index c38de2ae72c4e..518edd7d28e8c 100644 --- a/Mathlib/Order/Monotone/Basic.lean +++ b/Mathlib/Order/Monotone/Basic.lean @@ -238,43 +238,31 @@ theorem strictAntiOn_toDual_comp_iff : StrictAntiOn (toDual ∘ f : α → βᵒ Iff.rfl #align strict_anti_on_to_dual_comp_iff strictAntiOn_toDual_comp_iff -protected theorem Monotone.dual (hf : Monotone f) : Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) := - swap hf -#align monotone.dual Monotone.dual +theorem monotone_dual_iff : Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Monotone f := by + rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff] -protected theorem Antitone.dual (hf : Antitone f) : Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) := - swap hf -#align antitone.dual Antitone.dual +theorem antitone_dual_iff : Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Antitone f := by + rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff] -protected theorem MonotoneOn.dual (hf : MonotoneOn f s) : - MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s := - swap₂ hf -#align monotone_on.dual MonotoneOn.dual +theorem monotone_on_dual_iff : MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s := by + rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff] -protected theorem AntitoneOn.dual (hf : AntitoneOn f s) : - AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s := - swap₂ hf -#align antitone_on.dual AntitoneOn.dual +theorem antitone_on_dual_iff : AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s := by + rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff] -protected theorem StrictMono.dual (hf : StrictMono f) : - StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) := - swap hf -#align strict_mono.dual StrictMono.dual +theorem strict_mono_dual_iff : StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f := by + rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff] -protected theorem StrictAnti.dual (hf : StrictAnti f) : - StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) := - swap hf -#align strict_anti.dual StrictAnti.dual +theorem strict_anti_dual_iff : StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f := by + rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff] -protected theorem StrictMonoOn.dual (hf : StrictMonoOn f s) : - StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s := - swap₂ hf -#align strict_mono_on.dual StrictMonoOn.dual +theorem strict_mono_on_dual_iff : + StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictMonoOn f s := by + rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff] -protected theorem StrictAntiOn.dual (hf : StrictAntiOn f s) : - StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s := - swap₂ hf -#align strict_anti_on.dual StrictAntiOn.dual +theorem strict_anti_on_dual_iff : + StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictAntiOn f s := by + rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff] alias antitone_comp_ofDual_iff ↔ _ Monotone.dual_left #align monotone.dual_left Monotone.dual_left @@ -324,6 +312,30 @@ alias strictAntiOn_toDual_comp_iff ↔ _ StrictMonoOn.dual_right alias strictMonoOn_toDual_comp_iff ↔ _ StrictAntiOn.dual_right #align strict_anti_on.dual_right StrictAntiOn.dual_right +alias monotone_dual_iff ↔ _ Monotone.dual +#align monotone.dual Monotone.dual + +alias antitone_dual_iff ↔ _ Antitone.dual +#align antitone.dual Antitone.dual + +alias monotone_on_dual_iff ↔ _ MonotoneOn.dual +#align monotone_on.dual MonotoneOn.dual + +alias antitone_on_dual_iff ↔ _ AntitoneOn.dual +#align antitone_on.dual AntitoneOn.dual + +alias strict_mono_dual_iff ↔ _ StrictMono.dual +#align strict_mono.dual StrictMono.dual + +alias strict_anti_dual_iff ↔ _ StrictAnti.dual +#align strict_anti.dual StrictAnti.dual + +alias strict_mono_on_dual_iff ↔ _ StrictMonoOn.dual +#align strict_mono_on.dual StrictMonoOn.dual + +alias strict_anti_on_dual_iff ↔ _ StrictAntiOn.dual +#align strict_anti_on.dual StrictAntiOn.dual + end OrderDual /-! ### Monotonicity in function spaces -/