Strictly monotone maps out of total preorders [UPSTREAM] #
A strictly monotone map out of a total preorder reflects ≤. On a linear order this is half of
mathlib's StrictMono.le_iff_le; on a total preorder only the reflection survives, since tied
elements may be mapped apart.
Upstream home: Mathlib/Order/Monotone/Basic.lean, beside Monotone.reflect_lt.
Main statements #
StrictMono.reflect_le: a strictly monotone map out of a total preorder reflects≤.
theorem
StrictMono.reflect_le
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Std.Total fun (x1 x2 : α) => x1 ≤ x2]
[Preorder β]
{f : α → β}
(hf : StrictMono f)
{a b : α}
(h : f a ≤ f b)
:
a ≤ b
A strictly monotone map out of a total preorder reflects ≤.