## Stream: general

### Topic: strict monotone maps

#### Johan Commelin (Feb 28 2019 at 08:19):

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 (Feb 28 2019 at 08:20):

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 (Feb 28 2019 at 08:21):

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?

Last updated: May 14 2021 at 13:24 UTC