strict monotone maps

Stream: general

[Johan Commelin]

I know very little about the hierarchy of order structures in mathlib. For the perfectoid project we do need a little bit of it. Yesterday I wrote the following helper file:

import order.basic
open function

variables {α : Type*} {β : Type*}

def strict_mono [preorder α] [preorder β] (f : α → β) :=
∀ a b, a < b → f a < f b

namespace strict_mono

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 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 b a h') h,
 λ h, (lt_or_eq_of_le h).elim (λ h', le_of_lt (H _ _ h')) (λ h', h' ▸ le_refl _)⟩

lemma injective (H : strict_mono f) : function.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

lemma monotone (H : strict_mono f) :
  monotone f :=
λ a b, iff.mpr $ H.le_iff_le

end strict_mono

section
variables [partial_order α] [partial_order β] {f : α → β}

lemma strict_mono_of_monotone_of_injective (h₁ : monotone f) (h₂ : injective f) :
  strict_mono f :=
λ a b h,
begin
  rw lt_iff_le_and_ne at ⊢ h,
  exact ⟨h₁ h.1, λ e, h.2 (h₂ e)⟩
end

end

[Johan Commelin]

Am I duplicating stuff that is already in mathlib, or does this have a place.
The word strict_mono appears in mathlib, but the definition is not there.

[Johan Commelin]

There is also order_embedding, and in particular of_monotone, but

def of_monotone [is_trichotomous α r] [is_asymm β s] (f : α → β) (H : ∀ a b, r a b → s (f a) (f b)) : r ≼o s := _

doesn't actually mention monotone or classes in the order hierarchy. Is this nevertheless the way we ought to go?