feat(algebra/order/functions): recursors and images under monotone ma…

…ps (#9505)

src/algebra/order/functions.lean

@@ -22,7 +22,7 @@ variables {α : Type u} {β : Type v}
 attribute [simp] max_eq_left max_eq_right min_eq_left min_eq_right
 
 section
-variables [linear_order α] [linear_order β] {f : α → β} {a b c d : α}
+variables [linear_order α] [linear_order β] {f : α → β} {s : set α} {a b c d : α}
 
 -- translate from lattices to linear orders (sup → max, inf → min)
 @[simp] lemma le_min_iff : c ≤ min a b ↔ c ≤ a ∧ c ≤ b := le_inf_iff
@@ -100,6 +100,22 @@ left_comm max max_comm max_assoc a b c
 theorem max.right_comm (a b c : α) : max (max a b) c = max (max a c) b :=
 right_comm max max_comm max_assoc a b c
 
+lemma monotone_on.map_max (hf : monotone_on f s) (ha : a ∈ s) (hb : b ∈ s) :
+  f (max a b) = max (f a) (f b) :=
+by cases le_total a b; simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]
+
+lemma monotone_on.map_min (hf : monotone_on f s) (ha : a ∈ s) (hb : b ∈ s) :
+  f (min a b) = min (f a) (f b) :=
+hf.dual.map_max ha hb
+
+lemma antitone_on.map_max (hf : antitone_on f s) (ha : a ∈ s) (hb : b ∈ s) :
+  f (max a b) = min (f a) (f b) :=
+hf.dual_right.map_max ha hb
+
+lemma antitone_on.map_min (hf : antitone_on f s) (ha : a ∈ s) (hb : b ∈ s) :
+  f (min a b) = max (f a) (f b) :=
+hf.dual.map_max ha hb
+
 lemma monotone.map_max (hf : monotone f) : f (max a b) = max (f a) (f b) :=
 by cases le_total a b; simp [h, hf h]
 
@@ -112,6 +128,19 @@ by cases le_total a b; simp [h, hf h]
 lemma antitone.map_min (hf : antitone f) : f (min a b) = max (f a) (f b) :=
 hf.dual.map_max
 
+lemma min_rec {p : α → Prop} {x y : α} (hx : x ≤ y → p x) (hy : y ≤ x → p y) : p (min x y) :=
+(le_total x y).rec (λ h, (min_eq_left h).symm.subst (hx h))
+  (λ h, (min_eq_right h).symm.subst (hy h))
+
+lemma max_rec {p : α → Prop} {x y : α} (hx : y ≤ x → p x) (hy : x ≤ y → p y) : p (max x y) :=
+@min_rec (order_dual α) _ _ _ _ hx hy
+
+lemma min_rec' (p : α → Prop) {x y : α} (hx : p x) (hy : p y) : p (min x y) :=
+min_rec (λ _, hx) (λ _, hy)
+
+lemma max_rec' (p : α → Prop) {x y : α} (hx : p x) (hy : p y) : p (max x y) :=
+max_rec (λ _, hx) (λ _, hy)
+
 theorem min_choice (a b : α) : min a b = a ∨ min a b = b :=
 by cases le_total a b; simp *