feat(order/basic): lemmas about strict_mono_incr_on (#4313)

Also move the section about `order_dual` up to use it in the proofs.

Non-BC API changes:

* Now `strict_mono_incr_on` and `strict_mono_decr_on` take `x` and `y` as `⦃⦄` args.

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -117,9 +117,9 @@ begin
           apply not_le_of_lt (trans ‹i < j› ‹j < y›) (le_max_of_mem ‹y ∈ t› ‹i ∈ t.max›) },
         { apply lt_of_le_of_lt _ ‹f i < f j› <|> apply lt_of_lt_of_le ‹f j < f i› _,
           rcases lt_or_eq_of_le (le_max_of_mem ‹x ∈ t› ‹i ∈ t.max›) with _ | rfl,
-          { apply le_of_lt (ht₁.2.2 _ ‹x ∈ t› i (mem_of_max ‹i ∈ t.max›) ‹x < i›) },
+          { apply le_of_lt (ht₁.2.2 ‹x ∈ t› (mem_of_max ‹i ∈ t.max›) ‹x < i›) },
           { refl } },
-        { apply ht₁.2.2 _ ‹x ∈ t› _ ‹y ∈ t› ‹x < y› } },
+        { apply ht₁.2.2 ‹x ∈ t› ‹y ∈ t› ‹x < y› } },
       -- Finally show that this new subsequence is one longer than the old one.
       { rw [card_insert_of_not_mem, ht₂],
         intro _,

src/data/set/function.lean

@@ -551,6 +551,16 @@ end
 
 end set
 
+lemma strict_mono_incr_on.inj_on [linear_order α] [preorder β] {f : α → β} {s : set α}
+  (H : strict_mono_incr_on f s) :
+  s.inj_on f :=
+λ x hx y hy hxy, show ordering.eq.compares x y, from (H.compares hx hy).1 hxy
+
+lemma strict_mono_decr_on.inj_on [linear_order α] [preorder β] {f : α → β} {s : set α}
+  (H : strict_mono_decr_on f s) :
+  s.inj_on f :=
+@strict_mono_incr_on.inj_on α (order_dual β) _ _ f s H
+
 namespace function
 
 open set

src/order/basic.lean

@@ -131,15 +131,105 @@ lemma strict_mono_id [has_lt α] : strict_mono (id : α → α) := λ a b, id
 /-- A function `f` is strictly monotone increasing on `t` if `x < y` for `x,y ∈ t` implies
 `f x < f y`. -/
 def strict_mono_incr_on [has_lt α] [has_lt β] (f : α → β) (t : set α) : Prop :=
-∀ (x ∈ t) (y ∈ t), x < y → f x < f y
+∀ ⦃x⦄ (hx : x ∈ t) ⦃y⦄ (hy : y ∈ t), x < y → f x < f y
+
 /-- A function `f` is strictly monotone decreasing on `t` if `x < y` for `x,y ∈ t` implies
 `f y < f x`. -/
 def strict_mono_decr_on [has_lt α] [has_lt β] (f : α → β) (t : set α) : Prop :=
-∀ (x ∈ t) (y ∈ t), x < y → f y < f x
+∀ ⦃x⦄ (hx : x ∈ t) ⦃y⦄ (hy : y ∈ t), x < y → f y < f x
+
+/-- Type tag for a set with dual order: `≤` means `≥` and `<` means `>`. -/
+def order_dual (α : Type*) := α
+
+namespace order_dual
+instance (α : Type*) [h : nonempty α] : nonempty (order_dual α) := h
+instance (α : Type*) [has_le α] : has_le (order_dual α) := ⟨λx y:α, y ≤ x⟩
+instance (α : Type*) [has_lt α] : has_lt (order_dual α) := ⟨λx y:α, y < x⟩
+
+-- `dual_le` and `dual_lt` should not be simp lemmas:
+-- they cause a loop since `α` and `order_dual α` are definitionally equal
+
+lemma dual_le [has_le α] {a b : α} :
+  @has_le.le (order_dual α) _ a b ↔ @has_le.le α _ b a := iff.rfl
+
+lemma dual_lt [has_lt α] {a b : α} :
+  @has_lt.lt (order_dual α) _ a b ↔ @has_lt.lt α _ b a := iff.rfl
+
+lemma dual_compares [has_lt α] {a b : α} {o : ordering} :
+  @ordering.compares (order_dual α) _ o a b ↔ @ordering.compares α _ o b a :=
+by { cases o, exacts [iff.rfl, eq_comm, iff.rfl] }
+
+instance (α : Type*) [preorder α] : preorder (order_dual α) :=
+{ le_refl  := le_refl,
+  le_trans := assume a b c hab hbc, hbc.trans hab,
+  lt_iff_le_not_le := λ _ _, lt_iff_le_not_le,
+  .. order_dual.has_le α,
+  .. order_dual.has_lt α }
+
+instance (α : Type*) [partial_order α] : partial_order (order_dual α) :=
+{ le_antisymm := assume a b hab hba, @le_antisymm α _ a b hba hab, .. order_dual.preorder α }
+
+instance (α : Type*) [linear_order α] : linear_order (order_dual α) :=
+{ le_total := assume a b:α, le_total b a, .. order_dual.partial_order α }
+
+instance (α : Type*) [decidable_linear_order α] : decidable_linear_order (order_dual α) :=
+{ decidable_le := show decidable_rel (λa b:α, b ≤ a), by apply_instance,
+  decidable_lt := show decidable_rel (λa b:α, b < a), by apply_instance,
+  .. order_dual.linear_order α }
+
+instance : Π [inhabited α], inhabited (order_dual α) := id
+
+end order_dual
+
+namespace strict_mono_incr_on
+
+variables [linear_order α] [preorder β] {f : α → β} {s : set α} {x y : α}
+
+lemma le_iff_le (H : strict_mono_incr_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  f x ≤ f y ↔ x ≤ y :=
+⟨λ h, le_of_not_gt $ λ h', not_le_of_lt (H hy hx h') h,
+ λ h, (lt_or_eq_of_le h).elim (λ h', le_of_lt (H hx hy h')) (λ h', h' ▸ le_refl _)⟩
+
+lemma lt_iff_lt (H : strict_mono_incr_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  f x < f y ↔ x < y :=
+by simp only [H.le_iff_le, hx, hy, lt_iff_le_not_le]
+
+protected theorem compares (H : strict_mono_incr_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  ∀ {o}, ordering.compares o (f x) (f y) ↔ ordering.compares o x y
+| ordering.lt := H.lt_iff_lt hx hy
+| ordering.eq := ⟨λ h, le_antisymm ((H.le_iff_le hx hy).1 h.le) ((H.le_iff_le hy hx).1 h.symm.le),
+                   congr_arg _⟩
+| ordering.gt := H.lt_iff_lt hy hx
+
+end strict_mono_incr_on
+
+namespace strict_mono_decr_on
+
+variables [linear_order α] [preorder β] {f : α → β} {s : set α} {x y : α}
+
+lemma le_iff_le (H : strict_mono_decr_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  f x ≤ f y ↔ y ≤ x :=
+@strict_mono_incr_on.le_iff_le α (order_dual β) _ _ _ _ _ _ H hy hx
+
+lemma lt_iff_lt (H : strict_mono_decr_on f s) (hx : x ∈ s) (hy : y ∈ s) :
+  f x < f y ↔ y < x :=
+@strict_mono_incr_on.lt_iff_lt α (order_dual β) _ _ _ _ _ _ H hy hx
+
+protected theorem compares (H : strict_mono_decr_on f s) (hx : x ∈ s) (hy : y ∈ s) {o : ordering} :
+  ordering.compares o (f x) (f y) ↔ ordering.compares o y x :=
+order_dual.dual_compares.trans $
+  @strict_mono_incr_on.compares α (order_dual β) _ _ _ _ _ _ H hy hx _
+
+end strict_mono_decr_on
 
 namespace strict_mono
 open ordering function
 
+protected lemma strict_mono_incr_on [has_lt α] [has_lt β] {f : α → β} (hf : strict_mono f)
+  (s : set α) :
+  strict_mono_incr_on f s :=
+λ x hx y hy hxy, hf hxy
+
 lemma comp [has_lt α] [has_lt β] [has_lt γ] {g : β → γ} {f : α → β}
   (hg : strict_mono g) (hf : strict_mono f) :
   strict_mono (g ∘ f) :=
@@ -155,27 +245,18 @@ lemma id_le {φ : ℕ → ℕ} (h : strict_mono φ) : ∀ n, n ≤ φ n :=
 section
 variables [linear_order α] [preorder β] {f : α → β}
 
-lemma lt_iff_lt (H : strict_mono f) {a b} :
-  f a < f b ↔ a < b :=
-⟨λ h, ((lt_trichotomy b a)
-  .resolve_left $ λ h', lt_asymm h $ H h')
-  .resolve_left $ λ e, ne_of_gt h $ congr_arg _ e, @H _ _⟩
+lemma lt_iff_lt (H : strict_mono f) {a b} : f a < f b ↔ a < b :=
+(H.strict_mono_incr_on set.univ).lt_iff_lt trivial trivial
 
-lemma injective (H : strict_mono f) : injective f
-| a b e := ((lt_trichotomy a b)
-  .resolve_left $ λ h, ne_of_lt (H h) e)
-  .resolve_right $ λ h, ne_of_gt (H h) e
+protected theorem compares (H : strict_mono f) {a b} {o} :
+  compares o (f a) (f b) ↔ compares o a b :=
+(H.strict_mono_incr_on set.univ).compares trivial trivial
 
-theorem compares (H : strict_mono f) {a b} :
-  ∀ {o}, compares o (f a) (f b) ↔ compares o a b
-| lt := H.lt_iff_lt
-| eq := ⟨λ h, H.injective h, congr_arg _⟩
-| gt := H.lt_iff_lt
+lemma injective (H : strict_mono f) : injective f :=
+λ x y h, show compares eq x y, from H.compares.1 h
 
-lemma le_iff_le (H : strict_mono f) {a b} :
-  f a ≤ f b ↔ a ≤ b :=
-⟨λ h, le_of_not_gt $ λ h', not_le_of_lt (H h') h,
- λ h, (lt_or_eq_of_le h).elim (λ h', le_of_lt (H h')) (λ h', h' ▸ le_refl _)⟩
+lemma le_iff_le (H : strict_mono f) {a b} : f a ≤ f b ↔ a ≤ b :=
+(H.strict_mono_incr_on set.univ).le_iff_le trivial trivial
 
 lemma top_preimage_top (H : strict_mono f) {a} (h_top : ∀ p, p ≤ f a) (x : α) : x ≤ a :=
 H.le_iff_le.mp (h_top (f x))
@@ -223,46 +304,7 @@ lemma strict_mono_of_le_iff_le [preorder α] [preorder β] {f : α → β}
 
 end
 
-/-- Type tag for a set with dual order: `≤` means `≥` and `<` means `>`. -/
-def order_dual (α : Type*) := α
-
-namespace order_dual
-instance (α : Type*) [h : nonempty α] : nonempty (order_dual α) := h
-instance (α : Type*) [has_le α] : has_le (order_dual α) := ⟨λx y:α, y ≤ x⟩
-instance (α : Type*) [has_lt α] : has_lt (order_dual α) := ⟨λx y:α, y < x⟩
-
--- `dual_le` and `dual_lt` should not be simp lemmas:
--- they cause a loop since `α` and `order_dual α` are definitionally equal
-
-lemma dual_le [has_le α] {a b : α} :
-  @has_le.le (order_dual α) _ a b ↔ @has_le.le α _ b a := iff.rfl
-
-lemma dual_lt [has_lt α] {a b : α} :
-  @has_lt.lt (order_dual α) _ a b ↔ @has_lt.lt α _ b a := iff.rfl
-
-instance (α : Type*) [preorder α] : preorder (order_dual α) :=
-{ le_refl  := le_refl,
-  le_trans := assume a b c hab hbc, hbc.trans hab,
-  lt_iff_le_not_le := λ _ _, lt_iff_le_not_le,
-  .. order_dual.has_le α,
-  .. order_dual.has_lt α }
-
-instance (α : Type*) [partial_order α] : partial_order (order_dual α) :=
-{ le_antisymm := assume a b hab hba, @le_antisymm α _ a b hba hab, .. order_dual.preorder α }
-
-instance (α : Type*) [linear_order α] : linear_order (order_dual α) :=
-{ le_total := assume a b:α, le_total b a, .. order_dual.partial_order α }
-
-instance (α : Type*) [decidable_linear_order α] : decidable_linear_order (order_dual α) :=
-{ decidable_le := show decidable_rel (λa b:α, b ≤ a), by apply_instance,
-  decidable_lt := show decidable_rel (λa b:α, b < a), by apply_instance,
-  .. order_dual.linear_order α }
-
-instance : Π [inhabited α], inhabited (order_dual α) := id
-
-end order_dual
-
-/- order instances on the function space -/
+/-! ### Order instances on the function space -/
 
 instance pi.preorder {ι : Type u} {α : ι → Type v} [∀i, preorder (α i)] : preorder (Πi, α i) :=
 { le       := λx y, ∀i, x i ≤ y i,
@@ -330,6 +372,22 @@ def decidable_linear_order.lift {α β} [decidable_linear_order β] (f : α →
 instance subtype.preorder {α} [preorder α] (p : α → Prop) : preorder (subtype p) :=
 preorder.lift subtype.val
 
+@[simp] lemma subtype.mk_le_mk {α} [preorder α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} :
+  (⟨x, hx⟩ : subtype p) ≤ ⟨y, hy⟩ ↔ x ≤ y :=
+iff.rfl
+
+@[simp] lemma subtype.mk_lt_mk {α} [preorder α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y} :
+  (⟨x, hx⟩ : subtype p) < ⟨y, hy⟩ ↔ x < y :=
+iff.rfl
+
+@[simp, norm_cast] lemma subtype.coe_le_coe {α} [preorder α] {p : α → Prop} {x y : subtype p} :
+  (x : α) ≤ y ↔ x ≤ y :=
+iff.rfl
+
+@[simp, norm_cast] lemma subtype.coe_lt_coe {α} [preorder α] {p : α → Prop} {x y : subtype p} :
+  (x : α) < y ↔ x < y :=
+iff.rfl
+
 instance subtype.partial_order {α} [partial_order α] (p : α → Prop) :
   partial_order (subtype p) :=
 partial_order.lift subtype.val subtype.val_injective
@@ -448,6 +506,7 @@ def as_linear_order (α : Type u) := α
 instance {α} [inhabited α] : inhabited (as_linear_order α) :=
 ⟨ (default α : α) ⟩
 
-instance as_linear_order.linear_order {α} [partial_order α] [is_total α (≤)] : linear_order (as_linear_order α) :=
+instance as_linear_order.linear_order {α} [partial_order α] [is_total α (≤)] :
+  linear_order (as_linear_order α) :=
 { le_total := @total_of α (≤) _,
   .. (_ : partial_order α) }

src/order/rel_iso.lean

@@ -281,6 +281,10 @@ theorem map_le_iff : ∀ {a b}, a ≤ b ↔ (f a) ≤ (f b) := f.map_rel_iff'
 theorem map_lt_iff : ∀ {a b}, a < b ↔ (f a) < (f b) :=
 f.lt_embedding.map_rel_iff'
 
+protected theorem monotone : monotone f := λ x y, f.map_le_iff.1
+
+protected theorem strict_mono : strict_mono f := λ x y, f.map_lt_iff.1
+
 protected theorem acc (a : α) : acc (<) (f a) → acc (<) a :=
 f.lt_embedding.acc a
 
@@ -460,6 +464,23 @@ lemma mul_apply (e₁ e₂ : r ≃r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x
 
 end rel_iso
 
+namespace order_iso
+
+/-- Reinterpret an order isomorphism as an order embedding-/
+def to_order_embedding [has_le α] [has_le β] (e : α ≃o β) : α ↪o β :=
+e.to_rel_embedding
+
+@[simp] lemma coe_to_order_embedding [has_le α] [has_le β] (e : α ≃o β) :
+  ⇑(e.to_order_embedding) = e := rfl
+
+variables [preorder α] [preorder β]
+
+protected lemma monotone (e : α ≃o β) : monotone e := e.to_order_embedding.monotone
+
+protected lemma strict_mono (e : α ≃o β) : strict_mono e := e.to_order_embedding.strict_mono
+
+end order_iso
+
 /-- A subset `p : set α` embeds into `α` -/
 def set_coe_embedding {α : Type*} (p : set α) : p ↪ α := ⟨subtype.val, @subtype.eq _ _⟩